SMT (HCSS'13)

file

Visible to the public Thwarting Themida: Unpacking Malware with SMT Solvers

ABSTRACT

Malware analysis is one of the key problems in the realm of cybersecurity. Contemporary malware is nearly always protected from examination with the use of a "packer," a program designed to obscure its malicious functionality. In the past, packers used techniques such as compression, encryption or time locks to thwart analysis.

file

Visible to the public String Solvers for Web Security

ABSTRACT

Over the last decade, SMT solvers [1, 2] have made a huge impact in automatic bug-finding, analysis and verification of desktop software. More recently, string solvers are starting to have a similar impact on security analysis and vulnerability detection in web applications. String solvers provide a rich constraint language essential for security analysis of web applications, and recently have become efficient enough to be used at scale.

file

Visible to the public Cyber Defense Strategy

ABSTRACT

The briefing presents a strategy for analyzing and changing how we deal with defense of the nation's cyber assets.

file

Visible to the public Techniques for Scalable Symbolic Simulation

ABSTRACT

Symbolic simulation is a powerful technique for building mathematical models describing a program's results by simulating execution while interpreting inputs as symbolic variables. Such models can then be used to prove properties about the corresponding source program, including equivalence against a reference implementation.

file

Visible to the public Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties

The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system.