CS 698K: Designing Verifiably Secure Systems

Units: 3-0-0-0-9

Course Website:

Pre-requisites:

The course does not have any formal pre-requisites. Some background in systems programming and/or exposure to logic might be helpful.

 

Objectives

The objective of this course will be to understand, model, reason about and systematically defend against threats to system security. Students will learn the fundamentals of formal analysis and modeling, foundational security primitives, and how formal methods can be used to reason about the security of these primitives. The course will provide hands-on experience of applying formal tools for security analysis in order to automatically discover exploits and/or prove security properties of these systems.

 

Contents

	Broad Title	Topics	Num. Lect.
1.	Satisfiability	propositional  logic,  DPLL/CDCL/Chaff,  SAT  Extensions: QBF, AllSAT,  etc.	3
2.	SMT   and  applica- tions	first-order logic, SMT, approaches to SMT solving, symbolic execution using SMT	4
3.	Cryptographic Primitives	message authentication, symmetric-key encryption, public-key cryptography, modeling crypto in SMT	3
4.	Model Checking	explicit  state, symbolic bounded reachability, induction, abstraction/refinement,  CEGAR,  self-composition and hyper- properties, simulation/bi-simulation,  applications to security verification	5
5.	System       Security Primitives	isolation, access control, principle of least privilege, implementations of these in HW and SW, verification of these primitives: noninterference, static and dynamic information flow tracking	4
6.	Case studies, synthe- sis, machine learning	case studies with potential examples being enclave platforms, hypervisor security, e-voting; syntax-guided synthesis, applica- tions to/of  machine learning and statistical inference	4

 

Course Description

Ensuring computer systems remain secure is one of the fundamental challenges in computer science today. But what does a “secure system” mean, is it even possible to precisely and formally state the security requirements a system should satisfy? And even if that were possible, how would one verify that a system satisfies these requirements? Answering these questions will be the objective of the course.

This course will  introduce the fundamentals of formal modeling and verification – techniques for precisely reasoning about system behavior. This will be interleaved with a discussion of system security primitives: ranging from cryptography to systems’ primitives like isolation and access control combined with formal techniques for analyzing security of these primitives.  Students will gain hands- on experience practically applying formal tools to (i) find security exploits, and (ii) prove specific security properties. The course will conclude with case studies of system security verification, and a forward-looking discussion of potential research topics in this area.

 

References:

1. The Calculus of Computation: Decision Procedures with Applications to Verification, by Aaron R. Bradley and Zohar Manna.
2. Decision Procedures: An Algorithmic Point of View, Daniel Kroening and Ofer Strictman.
3. Principles of Model Checking, Christel Baier and Joost-Pieter Katoen.
4. Security Engineering: Ross Anderson.
5. Cryptography Engineering: Design Principles and Practical Applications, by Niels Ferguson, Bruce Schneier, and Tadayoshi Kohno.
6. Research Papers.