ASPIRE: Iterative specification synthesis for security

Kevin Zhijie Chen, Warren He, Devdatta Akhawe, Vijay D'Silva, Prateek Mittal, Dawn Song

Research output: Contribution to conferencePaperpeer-review

3 Scopus citations


How to perform a systematic security analysis of complex applications is a challenging and open question. Approaches based on formal verification are impeded due to the lack of application specifications. To address this challenge, we propose a framework, called ASPIRE, that enables analysts to automatically synthesize specifications from examples such as application input-output examples and system demonstrations. Our approach starts by synthesizing the initial candidate specifications in a domain specific language that conform to the examples, and iteratively prunes the candidate set by incorporating more user feedback. We implement a prototype of ASPIRE for synthesizing and checking specifications of web applications, although our approach is not limited to web security, and use it in three case studies to demonstrate the discovery of complex vulnerabilities in implementations of real world web applications. Our work is the first to design a general framework that leverages program synthesis techniques for security applications.

Original languageEnglish (US)
StatePublished - 2015
Event15th Workshop on Hot Topics in Operating Systems, HotOS 2015 - Warth-Weiningen, Switzerland
Duration: May 18 2015May 20 2015


Conference15th Workshop on Hot Topics in Operating Systems, HotOS 2015

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Information Systems


Dive into the research topics of 'ASPIRE: Iterative specification synthesis for security'. Together they form a unique fingerprint.

Cite this