This is an introductory course on formal analysis of software safety and security, covering the fundamental formalisms and various methods and tools for analyzing a software program to ensure its safety and security. The goal is to acquaint the students with fundamental analysis techniques tailored particularly for software safety and security and to prepare them for a professional career in the area. We will focus on static source code analysis interpreted in the most general sense and, for practicality, touch on some dynamic analysis techniques.

Yih-Kuen Tsay (蔡益坤), NTU IM Dept., 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)

Computer Programming and Discrete Mathematics

Class Notes and Selected Readings

We shall seek to strike a balance between depth and breadth, covering both the foundations and some of the more successful techniques and tools. Below is a tentative list of topics and their schedule:

• Introduction: Properties of a Software Program (.5 week: ) [slides]
• Fundations: Formal Logic (1.5 weeks: ) [slides:Propositional Logic, First-Order Logic; notes: Natural Deduction]
• Verification Tools: Coq (2 weeks: ) [slides; notes:Tactics for Natural Deduction in Coq]
• Methods: Hoare Logic (I) (2 weeks: ) [slides:Hoare Logic, notes: Rules of Hoare Logic, Proofs with Hoare Logic]
• Methods: Predicate Transformers (1 week: ) [slides]
• Methods: Hoare Logic (II) (1 week: ) [slides]
• Verification Tools: Frama-C + Plugins (2 weeks: ) [slides: Frama-C and ACSL, Frama-C with Coq; examples:Frama-C Examples]
• Methods: Owicki-Gries Method for Concurrent Programs (1 week: ) [slides]
• Final Exam (2022/??/??)
• Broader Picture: An Overview of Static Software Analysis (1 week: ) [slides]
• Wrap-Up Discussions (1 week: )

Homework Assignments 20%, Participation 10%, Final Exam 40%, Term Paper/Report 30%.

1. Software Safety vs. Security: What's the Difference?.
2. Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985. (Note: click on the link to author's free download site.)
3. Proof Theory and Automated Deduction, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
4. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
5. Foundations for Programming Languages, J.C. Mitchell, The MIT Press, 1996.
6. Formal Syntax and Semantics of Programming Languages, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
7. Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
8. Introduction to C program proof with Frama-C and its WP plugin, Allan Blanchard, 2020.
9. Software Foundations, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. (Note: click on the link to authors' free download site.)
10. Certified Programming with Dependent Types , A. Chilipala. (Note: click on the link to author's free download site.)
11. The Formal Methods Page: http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.)