1.      Proof-Carrying Code

The aim of this project is to develop an environment for proof-carrying code within which the Poitín theorem prover can be used.

Proof-carrying code [Necula, 1997] is a technique that can be used for safe execution of untrusted code. Typically, a code receiver establishes a set of safety rules that guarantee safe behavior of programs, and the code producer creates a formal safety proof that proves, for the untrusted code, adherence to the safety rules. Then, the receiver is able to use a simple and fast proof validator to check, with certainty, that the proof is valid and hence the untrusted code is safe to execute. The main advantage of this approach is that although there might be a large amount of effort in establishing and formally proving the safety of the untrusted code, almost the entire burden of doing this is on the code producer. The code consumer, on the other hand, has only to perform a fast, simple, and easy to trust proof-checking process.

Current approaches to proof-carrying code can only prove very simple properties of code such as type-safety. Ideally, we would like to be able to prove more complex properties of code such as security and functional properties. The Poitín theorem prover [Hamilton, 2005] can be used to prove such properties fully automatically (i.e. without expert user guidance). Poitín works by first of all distilling code into more efficient equivalent code, on which the required properties can be quickly verified. The majority of the computational power required is in the original distillation of the code. It is therefore proposed that this distillation should be performed by the code producer, and the verification of the properties of this distilled code be performed by the code consumer.

This project will involve developing an environment within which programs can be written (in the language recognised by Poitín) and properties can be specified and verified. For the code producer, it should be possible for the code producer to distill this developed code and then make it available for code consumers. Code consumers can then download this code and verify that it has the desired properties.

2.      A Development Environment for the B-Method

The aim of this project is to develop a user-friendly environment within which the B-method is easy to use.

Current publicly-available tools for development using the B-method suffer from a few drawbacks. Click’n’prove is not easy to use, and the need to interact with a theorem prover in order to be able to discharge proof obligations is particularly difficult for the user. ProB provides a more usable interface, but can only be used for finite-state models in which the number of states is kept fairly small as it makes use of model checking rather than theorem proving.

In this project, we propose the development of a new environment which overcomes these disadvantages. The editor and type checker used within ProB can also be used for this environment (these can be obtained from http://lifc.univ-fcomte.fr/~tatibouet/JBTOOLS). In order to allow the verification of models of unrestricted size without the need for user interaction, the fully automatic theorem prover Poitín [Hamilton, 2005] can be used. This project will therefore involve generating proof obligations from B specifications, and then transforming them into a form which can be used by Poitín in order to allow them to be automatically discharged.

3. User Interface for a Theorem Prover

Theorem provers are very useful tools for mechanical verification, but they have notoriously poor user interfaces. This project will involve developing a user interface for the fully automatic theorem prover Poitín [Hamilton, 2005] which makes it easier to use. This interface will allow the user to enter conjectures which Poitín can then attempt to prove. It will also allow users to enter logical specifications of programs, and to generate programs which meet these specifications from them (this functionality is already provided by Poitín, but not in a very easy to use way). The interface could also help the user to understand the generated proofs by allowing the user to step through the proofs and by displaying them graphically.

References

[Hamilton, 2005] G.W. Hamilton, “Poitín: Distilling Theorems From Conjectures”,
Proceedings of The Twelfth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Newcastle-Upon-Tyne, England, July 2005, To appear in Electronic Notes in Theoretical Computer Science

[Necula, 1997] George C. Necula, “Proof-Carrying Code”,   Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997