A Proof-Carrying-Code Infrastructure for Resources

This paper tackles the issue of increasing dependability of distributed systems in the presence of mobile code. To this end we present a complete proof-carrying-code (PCC) infrastructure for independent and automatic certification of resource bounds of mobile JVM programs. This includes a certifying compiler for a high-level language, which produces a certificate of bounded heap consumption, and independent certificate validation, realised via proof-checking, on the code-consumer side. Thus, we are now in a position to automatically infer linear upper bounds on the heap consumption of a strict, first-order functional language, generate a certificate encoding a formal proof of such bounded heap consumption and independently validate this certificate at the consumer side by checking the certificate. This prevents mobile code from exhausting resources on the local machine.