TY - GEN
T1 - A proof-carrying-code infrastructure for resources
AU - Loidl, Hans Wolfgang
AU - MacKenzie, Kenneth
AU - Jost, Steffen
AU - Beringer, Lennart
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
KW - Program verification
KW - Proof-carrying-code
KW - Resource analysis
UR - http://www.scopus.com/inward/record.url?scp=70350755621&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350755621&partnerID=8YFLogxK
U2 - 10.1109/LADC.2009.13
DO - 10.1109/LADC.2009.13
M3 - Conference contribution
AN - SCOPUS:70350755621
SN - 9780769537603
T3 - Proceedings - 2009 4th Latin-American Symposium on Dependable Computing, LADC 2009
SP - 127
EP - 134
BT - Proceedings - 2009 4th Latin-American Symposium on Dependable Computing, LADC 2009
T2 - 2009 4th Latin-American Symposium on Dependable Computing, LADC 2009
Y2 - 1 September 2009 through 4 September 2009
ER -