Taxonomic Search: File

Results 11 - 20 of 1434

Results

file

Thwarting Themida: Unpacking Malware with SMT Solvers

Submitted by Katie Dey on Tue, 05/14/2013 - 1:02pm. Contributors:

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.

  • 529.21 KB
  • 0 views
  • 8 downloads
  • Download
file

String Solvers for Web Security

Submitted by Katie Dey on Tue, 05/14/2013 - 12:55pm. Contributor:

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

Cyber Defense Strategy

Submitted by Katie Dey on Tue, 05/14/2013 - 12:42pm. Contributor:

ABSTRACT

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

file

Techniques for Scalable Symbolic Simulation

Submitted by Katie Dey on Mon, 05/13/2013 - 5:00pm. Contributor:

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

Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties

Submitted by Katie Dey on Mon, 05/13/2013 - 4:40pm. Contributor:

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.

  • 664.09 KB
  • 0 views
  • 11 downloads
  • Download
file

Automatic Theorem Proving and SMT

Submitted by Katie Dey on Mon, 05/13/2013 - 4:24pm. Contributor:

ABSTRACT

file

You Can't Touch This

Submitted by Katie Dey on Mon, 05/13/2013 - 3:16pm. Contributor:

ABSTRACT

JavaScript provides access to all resources via object properties. An access control mechanism that protects confidential information for such a language has to gauge traversals of the object graph. We propose a domain specific language to specify sets of objects, assign read and write permissions to them, and enforce these permissions in limited scopes of a program. To obtain complete interposition, we build the enforcement mechanism into the scripting engine.

file

Verifying JavaScript and Creating Foundations for the Web

Submitted by Katie Dey on Mon, 05/13/2013 - 3:02pm. Contributor:

ABSTRACT

file

JSCert: Certifying JavaScript

Submitted by Katie Dey on Mon, 05/13/2013 - 2:42pm. Contributor:

ABSTRACT

JavaScript has become the most widely used language for client- side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.