<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:x="urn:schemas-microsoft-com:office:excel" xmlns:p="urn:schemas-microsoft-com:office:powerpoint" xmlns:a="urn:schemas-microsoft-com:office:access" xmlns:dt="uuid:C2F41010-65B3-11d1-A29F-00AA00C14882" xmlns:s="uuid:BDC6E3F0-6DA3-11d1-A2A3-00AA00C14882" xmlns:rs="urn:schemas-microsoft-com:rowset" xmlns:z="#RowsetSchema" xmlns:b="urn:schemas-microsoft-com:office:publisher" xmlns:ss="urn:schemas-microsoft-com:office:spreadsheet" xmlns:c="urn:schemas-microsoft-com:office:component:spreadsheet" xmlns:odc="urn:schemas-microsoft-com:office:odc" xmlns:oa="urn:schemas-microsoft-com:office:activation" xmlns:html="http://www.w3.org/TR/REC-html40" xmlns:q="http://schemas.xmlsoap.org/soap/envelope/" xmlns:rtc="http://microsoft.com/officenet/conferencing" xmlns:D="DAV:" xmlns:Repl="http://schemas.microsoft.com/repl/" xmlns:mt="http://schemas.microsoft.com/sharepoint/soap/meetings/" xmlns:x2="http://schemas.microsoft.com/office/excel/2003/xml" xmlns:ppda="http://www.passport.com/NameSpace.xsd" xmlns:ois="http://schemas.microsoft.com/sharepoint/soap/ois/" xmlns:dir="http://schemas.microsoft.com/sharepoint/soap/directory/" xmlns:ds="http://www.w3.org/2000/09/xmldsig#" xmlns:dsp="http://schemas.microsoft.com/sharepoint/dsp" xmlns:udc="http://schemas.microsoft.com/data/udc" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:sub="http://schemas.microsoft.com/sharepoint/soap/2002/1/alerts/" xmlns:ec="http://www.w3.org/2001/04/xmlenc#" xmlns:sp="http://schemas.microsoft.com/sharepoint/" xmlns:sps="http://schemas.microsoft.com/sharepoint/soap/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:udcs="http://schemas.microsoft.com/data/udc/soap" xmlns:udcxf="http://schemas.microsoft.com/data/udc/xmlfile" xmlns:udcp2p="http://schemas.microsoft.com/data/udc/parttopart" xmlns:wf="http://schemas.microsoft.com/sharepoint/soap/workflow/" xmlns:dsss="http://schemas.microsoft.com/office/2006/digsig-setup" xmlns:dssi="http://schemas.microsoft.com/office/2006/digsig" xmlns:mdssi="http://schemas.openxmlformats.org/package/2006/digital-signature" xmlns:mver="http://schemas.openxmlformats.org/markup-compatibility/2006" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns:mrels="http://schemas.openxmlformats.org/package/2006/relationships" xmlns:spwp="http://microsoft.com/sharepoint/webpartpages" xmlns:ex12t="http://schemas.microsoft.com/exchange/services/2006/types" xmlns:ex12m="http://schemas.microsoft.com/exchange/services/2006/messages" xmlns:pptsl="http://schemas.microsoft.com/sharepoint/soap/SlideLibrary/" xmlns:spsl="http://microsoft.com/webservices/SharePointPortalServer/PublishedLinksService" xmlns:Z="urn:schemas-microsoft-com:" xmlns:st="&#1;" xmlns="http://www.w3.org/TR/REC-html40">

<head>
<meta http-equiv=Content-Type content="text/html; charset=iso-8859-1">
<meta name=Generator content="Microsoft Word 12 (filtered medium)">
<style>
<!--
 /* Font Definitions */
 @font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
 /* Style Definitions */
 p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0in;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
span.EmailStyle17
        {mso-style-type:personal-reply;
        font-family:"Arial","sans-serif";
        color:blue;
        font-weight:normal;
        font-style:normal;
        text-decoration:none none;}
.MsoChpDefault
        {mso-style-type:export-only;}
@page Section1
        {size:8.5in 11.0in;
        margin:1.0in 1.0in 1.0in 1.0in;}
div.Section1
        {page:Section1;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext="edit">
  <o:idmap v:ext="edit" data="1" />
 </o:shapelayout></xml><![endif]-->
</head>

<body lang=EN-US link=blue vlink=purple>

<div class=Section1>

<p class=MsoNormal><span style='color:blue'>Matt Meola will present his
research seminar/general exam on Wednesday May 13 <o:p></o:p></span></p>

<p class=MsoNormal><span style='color:blue'>at 2PM in Room 402.  The members of
his committee are:  David Walker, advisor, <o:p></o:p></span></p>

<p class=MsoNormal><span style='color:blue'>Andrew Appel, and Ed Felten. 
Everyone is invited to attend his talk, and those faculty <o:p></o:p></span></p>

<p class=MsoNormal><span style='color:blue'>wishing to remain for the oral exam
following are welcome to do so.  His abstract and <o:p></o:p></span></p>

<p class=MsoNormal><span style='color:blue'>reading list follow below.<o:p></o:p></span></p>

<p class=MsoNormal><span style='color:blue'>-------------------------------------------<o:p></o:p></span></p>

<p class=MsoNormal><br>
Abstract<br>
--------<br>
As semiconductor manufacturing technologies improve, feature sizes get<br>
smaller, and transistors more densely packed, computer users face an<br>
ever-increasing chance that cosmic rays and other sources of high energy<br>
particles will disrupt the workings of their processors. When implementing<br>
cryptographic algorithms, security protocols, long-running simulations, and<br>
safety-critical systems, software developers must consider the possibility<br>
that such intermittent hardware faults will cause irreparable harm to their<br>
applications. Boneh, DeMillo, and Lipton were the first to show that a<br>
single fault could be exploited to break common implementations of RSA.<br>
Others followed, demonstrating exploits of cryptosystems and runtime systems<br>
achieved by inducing transient faults.<br>
<br>
To support the higher degrees of confidence required in these critical<br>
applications, we have developed a new logic for reasoning about faulty<br>
programs. Our logic allows the verification of programs even in the presence<br>
of transient faults. It operates over a standard language of imperative<br>
while programs augmented with a single new instruction to indicate the<br>
possibility of faults at particular program points. The logic itself is a<br>
relative of Separation Logic in which the separating conjunction is used to<br>
reason about the limits to which faults may affect different parts of<br>
program state.<br>
<br>
As much as is practical, the logic is intended to be agnostic of the<br>
particular model used to decide when faults may occur. In particular, our<br>
current work deals with standard fault models that allow a certain maximum<br>
number of faults to occur in program variables in a single run of the<br>
program and limits faults according to how they affect data (typically<br>
either allowing only a single bit flip or allowing arbitrary changes in<br>
value). Faults in control-flow and many control logic faults (such as<br>
misinterpretation of opcodes) are ignored, except where they can be<br>
simulated by data faults.<br>
<br>
We prove the logic is sound and illustrate how to use it on several simple<br>
examples, including a simplified, idealized version of the RSA message<br>
signing algorithm. We show how the introduction of a modal connective<br>
helps to simplify program assertions and facilitate the reasoning process.<br>
<br>
<br>
Books<br>
-----<br>
Pierce, B.C. Types and Programming Languages. MIT Press, 2002.<br>
Ch 1, 2, 4, 5 of &nbsp; Huth, M.R.A. and Ryan, M.D. Logic in Computer Science:
Modelling and Reasoning about Systems. Cambridge University Press, 2000.<br>
<br>
<br>
Papers<br>
------<br>
[1] Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., and Whelan, C. The
Sorcerer&#8217;s Apprentice Guide to Fault Attacks. Proc. IEEE, Vol. 94.
370-382, Feb. 2006.<br>
[2] Barthe, G., Grégoire, B., and Zanella Béguelin, S. 2009. Formal
certification of code-based cryptographic proofs. In Proceedings of the 36th
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(Savannah, GA, USA, January 21 - 23, 2009). POPL '09. ACM, New York, NY,
90-101.<br>
[3] Boneh, D., DeMillo, R., and Lipton, R., On the importance of checking
cryptographic protocols for faults, Journal of Cryptology 14 (2001). 101­-119.<br>
[4] Chang, J., G. A. Reis and D. I. August. Non-Uniform Fault Tolerance. In
Proceedings of the 2nd Workshop on Architectural Reliability (WAR), December
2006.<br>
[5] Ishtiaq, S. and O'Hearn, P. Bi as an assertion language for mutable data
structures. In Proceedings of the 28th ACM Symposium on Principles of
Programming Languages, London, United Kingdom, 2001, 14­-26.<br>
[6] Perry, F., Mackey, L., Reis, G. A., Ligatti, J., August, D. I., and Walker,
D. 2007. Fault-tolerant typed assembly language. In Proceedings of the 2007 ACM
SIGPLAN Conference on Programming Language Design and Implementation (San
Diego, California, USA, June 10 - 13, 2007). PLDI '07. ACM, New York, NY,
42-53.<br>
[7] Rebaudengo, M., Sonza Reorda, M., Torchiano, M., and Violante, M.,
Soft-error Detection through Software Fault-Tolerance techniques, in: IEEE
International Symposium on Defect and Fault Tolerance in VLSI Systems, 1999,
210-218.<br>
[8] Reis, G. A., Chang, J., and August, D. I. 2007. Automatic Instruction-Level
Software-Only Recovery. IEEE Micro 27, 1 (Jan. 2007), 36-47.<br>
[9] Shirvani, P. P., Saxena, N., and McCluskey, E. J. 2000.
Software-implemented EDAC protection against SEUs. In IEEE Transactions on
Reliability. Vol. 49. 273&#8211;284.<br>
[10] Walker, D., Mackey, L., Ligatti, J., Reis, G. A., and August, D. I. 2006.
Static typing for a faulty lambda calculus. In Proceedings of the Eleventh ACM
SIGPLAN international Conference on Functional Programming (Portland, Oregon,
USA, September 16 - 21, 2006). ICFP '06. ACM, New York, NY, 38-49.<o:p></o:p></p>

</div>

</body>

</html>