Formal methods are mathematical techniques for the specification, design, and verification of software and hardware systems. In the context of security, formal methods provide rigorous tools to model and analyze systems for potential vulnerabilities and ensure compliance with security policies. These methods enable the precise definition of security properties, such as confidentiality, integrity, and privacy, and allow for automated verification to detect flaws that may be overlooked by traditional testing. By applying formal techniques such as model checking, theorem proving, and formal specification languages, developers can build systems with provable security guarantees. The course consists of a series of lectures on different formalisms and methods that have been developed to reason about security and privacy properties. Topics include program verification through relational Hoare logic and its probabilistic extensions, the specification and verification of hyperproperties, formal verification of cryptographic protocols, and techniques for quantitative information flow analysis and verification.
Hazem Torfah
