Must be in the Computer Science Master's or Doctoral programs, or permission of instructor.

Software is often designed with vague and unprincipled notions of correctness, opening the door to security and privacy vulnerabilities. To teach students how to create software and systems with guarantees of correct and secure execution, this course explores the formal foundations of computer security through the lens of language-based security. Topics include types for security (e.g., information flow type systems, typed assembly, wasm),formal semantics, security policies and specification, safety- and hyper-properties, secure compilation, and lightweight verification techniques, such as model checking. Students will also do in-depth readings on cutting-edge research in this space.