Matt Meola will present his research seminar/general exam on Wednesday May 13

at 2PM in Room 402.  The members of his committee are:  David Walker, advisor,

Andrew Appel, and Ed Felten.  Everyone is invited to attend his talk, and those faculty

wishing to remain for the oral exam following are welcome to do so.  His abstract and

reading list follow below.

-------------------------------------------

Abstract
--------
As semiconductor manufacturing technologies improve, feature sizes get
smaller, and transistors more densely packed, computer users face an
ever-increasing chance that cosmic rays and other sources of high energy
particles will disrupt the workings of their processors. When implementing
cryptographic algorithms, security protocols, long-running simulations, and
safety-critical systems, software developers must consider the possibility
that such intermittent hardware faults will cause irreparable harm to their
applications. Boneh, DeMillo, and Lipton were the first to show that a
single fault could be exploited to break common implementations of RSA.
Others followed, demonstrating exploits of cryptosystems and runtime systems
achieved by inducing transient faults.

To support the higher degrees of confidence required in these critical
applications, we have developed a new logic for reasoning about faulty
programs. Our logic allows the verification of programs even in the presence
of transient faults. It operates over a standard language of imperative
while programs augmented with a single new instruction to indicate the
possibility of faults at particular program points. The logic itself is a
relative of Separation Logic in which the separating conjunction is used to
reason about the limits to which faults may affect different parts of
program state.

As much as is practical, the logic is intended to be agnostic of the
particular model used to decide when faults may occur. In particular, our
current work deals with standard fault models that allow a certain maximum
number of faults to occur in program variables in a single run of the
program and limits faults according to how they affect data (typically
either allowing only a single bit flip or allowing arbitrary changes in
value). Faults in control-flow and many control logic faults (such as
misinterpretation of opcodes) are ignored, except where they can be
simulated by data faults.

We prove the logic is sound and illustrate how to use it on several simple
examples, including a simplified, idealized version of the RSA message
signing algorithm. We show how the introduction of a modal connective
helps to simplify program assertions and facilitate the reasoning process.


Books
-----
Pierce, B.C. Types and Programming Languages. MIT Press, 2002.
Ch 1, 2, 4, 5 of   Huth, M.R.A. and Ryan, M.D. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2000.


Papers
------
[1] Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., and Whelan, C. The Sorcerer’s Apprentice Guide to Fault Attacks. Proc. IEEE, Vol. 94. 370-382, Feb. 2006.
[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.
[3] Boneh, D., DeMillo, R., and Lipton, R., On the importance of checking cryptographic protocols for faults, Journal of Cryptology 14 (2001). 101-119.
[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.
[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.
[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.
[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.
[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.
[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–284.
[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.