
<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 10pt; color: #000000'><br><div style="color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div>Joey Dodds will present his research seminar/general exam on Tuesday January 17 <br>at 1PM in Room 402.  The members of his committee are:  Andrew Appel (advisor), <br>David Walker, and Zeev Dvir.  Everyone is invited to attend his talk and those <br>faculty members wishing to remain for the oral exam following are welcome to do so.<br>His abstract and reading list follow below.<br>------------------------------<br><div><div style=""><br></div><div style="">Title: Machine-Checked Proofs of Conditional Information Flow</div><div style=""><br></div><div style="">Abstract:</div><div style=""> 

  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.  </div>


<div style="">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.</div>


<div style=""><br></div><div style="">   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.<br><br></div></div><div><div style="">Text books:</div><div style="">   <span style="white-space:pre">       </span><span style="white-space:pre">     </span> A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998 </div><div style=""><ul>


<li style="margin-left:15px">  B. Pierce. Types and Programming Languages. 2002.</li></ul></div><div style=""><br></div><div style="">Papers</div><div style="">  </div><div style=""><ul><li style="margin-left:15px">A. W. Appel. VeriSmall: Veriﬁed Smallfoot Shape Analysis. In First International Conf. on Certiﬁed Programs and Proofs Dec. 2011</li>


<li style="margin-left:15px">G. Necula. Proof-Carrying Code. In POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997.</li><li style="margin-left:15px">T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In POPL 2006. ACM Press, 2006.</li>


<li style="margin-left:15px">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.</li>


<li style="margin-left:15px">X. Leroy. A formally verified compiler back-end. In Journal of Automated Reasoning, 2009</li><li style="margin-left:15px">A. Sabelfeld, A. C. Myers. Language-Based Information-Flow Security. In IEEE Journal on Selected Areas in Communications, 2003 </li>


<li style="margin-left:15px">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.</li>


</ul></div><br></div></div>

</div><br></div></body></html>