Practical Security Verification

Security Verification Overview

Computers form the backbone of any modern society, and often process large amounts of sensitive and private information. To help secure the software, and the sensitive data, a number of secure hardware-software and processor architectures have been proposed. These architectures incorporate novel protection and defense mechanisms directly in the hardware where they cannot be modified or bypassed, unlike software protections. However, due to lack of practical and scalable security verification tools and methodologies, very few of the proposed hardware security architectures have been commercially deployed. This project develops a security verification methodology that is applicable to different hardware-software security architectures. Researchers and designers will have a new method to systematically check their designs, and show to others the conditions under which they work. Hardware manufacturers will gain assurance to actually implement these security architectures in real products. In turn, customers will gain assurance about the secure hardware that protects their computations running on their devices or virtual machines running on remote cloud servers. Security architectures are important to customers and hardware manufacturers, however, security verification is needed to make them a reality.

Project Highlight

Verification of Resilience to Cache Side-channel attacks

This project develops methodology to verify a secure cache's resistance to cache side channel attacks.

  1. Tianwei Zhang and Ruby B. Lee, "New Models of Cache Architectures Characterizing Information Leakage from Cache Side," in Proceedings of Annual Computer Security Applications Conference (ACSAC), December 2014.

Verification of Cloud Computing Architecture

This project aims to develop security invariants and methodology that can be applied to verify hardware-enhanced cloud server architectures and minimize the attack surface in cloud computing.
  1. Jakub Szefer, "Architectures for Secure Cloud Computing Servers," PhD Thesis, Electrical Engineering Department, Princeton University, Princeton, NJ (2013)
  2. Tianwei Zhang and Ruby B. Lee, "Security Verification of Hardware-enabled Attestation Protocols," in Proceedings of the Workshop on Hardware and Architectural Support for Security and Privacy (HASP) (2012).
  3. Jakub Szefer, Tianwei Zhang and Ruby B. Lee, "Security Verification of Secure Processor Architectures and Systems," Princeton University Technical Report CE-L2017-002, August 2017.