- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Bld I, Microsoft Research-INRIA Joint Centre
Sound Automatic Implementation Generation and Monitoring of Security Protocol Implementations from Verified Formal Specifications.
Alfredo Pironti
Politecnico di Torino
The thesis is about the application of formal methods to the model-driven development (MDD) of security protocol implementations. The main goal is to improve the overall reliability and dependability of the final applications, by following a formally-justified development methodology.
In the proposed framework, the developer starts by writing and verifying an abstract, formal specification (in the Spi Calculus language) of the protocol to be implemented. From the formally verified specification, a Java application is then derived by iterative refinement steps. Each of these refinement steps is assisted by automatic tools, and is proved to be sound: that is, with each refinement step the developer gets closer to the final implementation, without breaching any security property already proved on the abstract specification.
When developing such methodology, essentially two main issues had to be solved: (i) the soundness relation between the generated Java code, and the original Spi Calculus model; and (ii) the interoperability of the generated application, so that it can adhere to already existing protocol standards. The first issue is solved by defining a simulation relation between Java and Spi Calculus, and by showing that our translation satisfies such simulation relation. The second issue is solved by letting the user implement the marshaling functions, and by giving sufficient conditions, so that such functions cannot compromise the security properties of the original protocol.
Since the proposed MDD approach only allows to generate new implementations, an alternative approach is proposed, in order to handle legacy implementations. In this case, the MDD approach is used to generate provably correct monitors for such legacy implementations. A monitor lets safe protocol sessions execute, and stops incorrect or malicious ones.
The overall methodology has been validated by developing a fully featured client for the SSH protocol, and a monitor for SSL servers.