Proof-Carrying Code for Extended Static Checking

Funded by the IRCSET Embark Initiative

IRCSET Fellow: Alan Morkan

It is widely acknowledged that there are numerous flaws in modern software, especially in relation to security. Therefore, it is necessary to bring about a change in the manner in which programmers take responsibility for the quality of their code. In order to achieve this, the main methodology proposed by computer scientists is the use of advanced tools and techniques to create bug-free software. Among the concepts advocated is Proof Carrying Code (PCC).

PCC attaches a formalised mathematical proof to program code that guarantees certain properties about the code (such as security, correctness, memory-usage, etc.). A certificate contains this proof and other related information. The verification of this certificate is used to establish trust with the code consumer. PCC technology has the potential to revolutionise security architectures for mobile code and global computing, and is receiving increased attention from leading industrial stakeholders in application areas with stringent security concerns. While PCC holds the promise of becoming a pivotal technology in next-generation security architectures, research has so far only considered very simple scenarios.

Our proposed research involves the development of a Proof Generating Extended Static Checker and an On-Device Proof Checker, two core elements of the PCC infrastructure.

A Proof Generating Extended Static Checker emits a proof for statically checked properties at the source code and bytecode level in a program. These proofs are embedded into a certificate for the corresponding bytecode.

On-Device Proof Checking represents the consumer side of PCC technology. When software is downloaded to a device, the On-Device Proof Checker takes the attached certificate and verifies its proof against the accompanying bytecode and specification. Any malicious modification of the code from the moment of compilation is automatically recognised. Viruses and other nefarious code are created by making such changes. An important aspect of such a checker is that it must run on all devices, even tiny devices such as smart cards or button-sized sensors. Developing a proof checker that can operate within the memory and CPU usage constraints of such devices is very challenging.