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 Sorcerers 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. 273284. [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.