[talks] J Dodds general exam

[Melissa M. Lawson]

Joey Dodds will present his research seminar/general exam on Tuesday January 17 
at 1PM in Room 402. The members of his committee are: Andrew Appel (advisor), 
David Walker, and Zeev Dvir. Everyone is invited to attend his talk and those 
faculty members wishing to remain for the oral exam following are welcome to do so. 
His abstract and reading list follow below. 
------------------------------ 




Title: Machine-Checked Proofs of Conditional Information Flow 


Abstract: 
Previous work proposed a compositional framework for stating and automatically verifying complex conditional information flow policies using a relational Hoare logic. The framework allows developers and verifiers to work directly with the source code using source-level code contracts. In this work, we extend that approach so that the algorithm for verifying code compliance to an information flow contract emits formal certificates of correctness that are checked in the Coq proof assistant. This framework is implemented in the context of SPARK -- a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems. 
This work puts in place a crucial element of our larger vision for end-to-end security assurance -- namely, the ability to leverage a formally verified compiler to provide a tool chain that enables us to prove that deployed executable code conforms to complex information flow policies stated as source-level contracts. 


The Coq code consists of a definition for the core SPARK language, operational semantics for the language, definitions for the form of certificates, and soundness proofs of the certificates with respect to the operational semantics. We will discuss these definitions and proofs, along with the challenges of formalizing a paper proof. Certificates for analyses such as ours can often blow up to an unmanageable size. We have taken steps towards mitigating this contract explosion including beginning an implementation of the analysis in Coq. We can prove that evidence always exists, guaranteeing that any precondition generated by the function is correct with respect to the operational semantics of the language without requiring the transmission of a large contract. 



Text books: 
A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998 


    * B. Pierce. Types and Programming Languages. 2002. 



Papers 



    * A. W. Appel. VeriSmall: Verified Smallfoot Shape Analysis. In First International Conf. on Certified Programs and Proofs Dec. 2011 
    * G. Necula. Proof-Carrying Code. In POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997. 
    * T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In POPL 2006. ACM Press, 2006. 
    * T. Amtoft, J. Hatcliff, and E. Rodrıguez. Precise and automated contract-based reasoning for verification and certification of information flow properties -of programs with arrays. In ESOP’10, volume 6012 of LNCS, pages 43–63, March 2010. 
    * X. Leroy. A formally verified compiler back-end. In Journal of Automated Reasoning, 2009 
    * A. Sabelfeld, A. C. Myers. Language-Based Information-Flow Security. In IEEE Journal on Selected Areas in Communications, 2003 
    * Boettcher, C., DeLong, R., Rushby, J., and Sifre, W. 2008. The mils component integration approach to secure information sharing. In 27th IEEE/AIAA Digital Avionics Systems Conference 2008. 


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20120111/925aa072/attachment.html>