From SE Wiki

Contents 1 Overview 2 News 3 Primary website 4 Members 4.1 Other Faculty 4.2 Students 4.3 External collaborators 5 Tools 6 Publications 7 Funding

Overview

The Verisec project aimed to apply advances in the field of formal verification to computer security. A major focus of the project was on using software model checking to verify the absence of implementation-level vulnerabilities in computer programs; notably, buffer overflows. We have developed a suite of code examples based on buffer overflows in open source software, called the Verisec suite, and have developed a technique based on proof templates to make the verification of the absence of buffer overflows more practical for software model checkers based on predicate abstraction and refinement.

News

Primary website

Members

Principal investigator: Marsha Chechik and David Lie

Other Faculty

• N/A

Students

• Thomas E. Hart
• Kelvin Ku

External collaborators

• Arie Gurfinkel --- SEI, CMU (UofT alumnus)

Tools

• PtYasm
• The Verisec Suite

Publications

• A Buffer Overflow Benchmark for Software Model Checkers. Kelvin Ku, Thomas E. Hart, Marsha Chechik, and David Lie. In Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE'07), Atlanta, Georgia, USA, November 2007.
• Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08), L'Aquila, Italy, September 2008.
• PTYASM: Software Model Checking with Proof Templates. Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08) --- Tools Demonstrations Track, L'Aquila, Italy, September 2008.
• Security Benchmarking using Partial Verification. Thomas E. Hart, Marsha Chechik, and David Lie. In Proc. 3rd USENIX Workshop on Hot Topics in Security (HotSec'08), San Jose, California, USA, July 2008.

Funding

MITACS and NSERC