Report on the NSF Workshop on Formal Methods for Security* Covers opportunities for formal methods across PL, OS, Privacy, and Architecture
Security as a new dimension in embedded system design
TLA+ Tools, Video Tutorials, and papers
MiniSat SAT Solver
CVC4 SMT Solver and Theorem Prover
Z3 SMT Solver and Theorem Prover
Z3 - guide tutorial
Alloy Language and tool for Relational Models
Cryptol Domain specific language for specifying crypto algorithms
Coq Formal proof management system
Kami Coq framework for bluespec-style hardware
Lean Theorem Prover
Dafny Verification-aware programming language
Whiley Language with extended static checking
Execution Leases: A Hardware-Supported Mechanism for Enforcing Strong Non-Interference*
Information Flow Isolation in I2C and USB*
Caisson: A Hardware Description Language for Secure Information Flow*
Theoretical Fundamentals of Gate Level Information Flow Tracking*
Inspection Resistant Memory: Architectural Support for Security from Physical Examination*
SurfNoC: A Low Latency and Provably Non-Interfering Approach to Secure Networks-On-Chip*
Sapper: A Language for Hardware-Level Security Policy Enforcement*
Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software
Secure Information Flow Verification with Mutable Dependent Types
Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis
Secure Dynamic Memory Scheduling Against Timing Channel Attacks
Lattice Priority Scheduling: Low-Overhead Timing Channel Protection for a Shared Memory Controller
A Hardware Design Language for Timing-Sensitive Information-Flow Security
Efficient Timing Channel Protection for On-Chip Networks
Aegis: A Single-Chip Secure Processor
Systematic Security Assessment at an Early Processor Design Stage
Practical, Lightweight Secure Inclusion of Third-Party Intellectual Property
Side-channel Vulnerability Factor: A Metric for Measuring Information Leakage
Tamper Evident Microprocessors
Understanding Contention-Based Channels and Using Them for Defense
PHANTOM: Practical Oblivious Computation in a Secure Processor
Towards Fast Hardware Memory Integrity Checking with Skewed Merkle Trees
Scalable Architectural Support for Trusted Software
Architecture for Protecting Critical Secrets in Microprocessors
New cache designs for thwarting software cache-based side channel attacks
Security Verification of Hardware-enabled Attestation Protocols
SPECS: A Lightweight Runtime Mechanism for Protecting Software from Security-Critical Processor Bugs
Overcoming an Untrusted Computing Base: Detecting and Removing Malicious Hardware Automatically
Bandwidth Hard Functions for ASIC Resistance
Secure Program Execution via Dynamic Information Flow Tracking
Design and Implementation of the Ascend Secure Processor
A Formal Foundation for Secure Remote Execution of Enclaves
Chasing Away RAts: Semantics and Evaluation for Relaxed Atomics on Heterogeneous Systems
Architecting Hierarchical Coherence Protocols for Push-button Parametric Verification
PVCoherence: Designing Flat Coherence Protocols for Scalable Verification
Fractal Consistency: Architecting the Memory System to Facilitate Verification
Specifying and Dynamically Verifying Address Translation-Aware Memory Consistency
Analyzing Formal Verification and Testing Efforts of Different Fault Tolerance Mechanisms
Using Speculation to Simplify Multiprocessor Design
Dynamic Verification of End-to-End Multiprocessor Invariants
Token coherence: decoupling performance and correctness
An Architecture Supporting Formal and Compositional Binary Analysis*
High Bandwidth Network Memory System Through Virtual Pipelines*
Observability Analysis of Embedded Software for Coverage-Directed Validation
Verification-Aware Microprocessor Design
Processor Verification with Precise Exceptions and Speculative Execution
Mostly-automated verification of low-level programs in computational separation logic
Machine-verified network controllers
Formal requirements for virtualizable third generation architectures
A Survey of Recent Advances in SAT-Based Formal Verification
GRASP: A Search Algorithm for Propositional Satisfiability
Chaff: Engineering an Efficient SAT Solver
The Quest for Efficient Boolean Satisfiability Solvers
Efficient Conflict Driven Learning in a Boolean Satisfiability Solver
Conflict-Driven Clause Learning SAT Solvers -- chapter in the Handbook of Satisfiability
Logic For Computer Science, Foundations of Automatic Theorem Proving, Jean H. Gallier -- for more background on Boolean logic
Satisfiability Modulo Theories
Lazy Satisfiability Modulo Theories
Satisfiability Modulo Theories: Introduction and Applications
Lemma Learning in SMT on Linear Constraints
Satisfiability Modulo Theories -- chapter in the Handbook on Model Checking
Formalizing DPLL-based Solvers for Propositional Satisfiability and for Satisfiability Modulo Theories -- slides with examples
SAT Beyond Propositional Satisfiability -- tutorial slides
SMT Solvers: Theory and Implementation -- tutorial slides
SMT-LIB -- The Satisfiability Modulo Theories Library
* papers on which the instructor is an author -- pretend they are good ;)