Abstract
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 language | English (US) |
---|---|
State | Published - 2015 |
Event | 15th Workshop on Hot Topics in Operating Systems, HotOS 2015 - Warth-Weiningen, Switzerland Duration: May 18 2015 → May 20 2015 |
Conference
Conference | 15th Workshop on Hot Topics in Operating Systems, HotOS 2015 |
---|---|
Country/Territory | Switzerland |
City | Warth-Weiningen |
Period | 5/18/15 → 5/20/15 |
All Science Journal Classification (ASJC) codes
- Computer Networks and Communications
- Hardware and Architecture
- Information Systems