Designing secure systems and validating security of existing systems are hard challenges facing our society. For implementing secure applications, a serious stumbling block lies in the generation of a correct system specification for a security policy. It is non-trivial for both system designers and end users to express their intent in terms of formal logic. Similar challenges plague users' trying to validate security properties of existing applications, such as web or cloud based services, which often have no formal specifications. Thus, there is an urgent need for mechanisms that can bridge the gap between expressions of user intent and system specifications. This research designs an approach and a system called Aspire that is able to translate user intent into security specifications.
Aspire takes as input, expressions of user intent such as a system demonstration, application input-output examples, or natural language. Aspire leverages recent developments in the field of automated synthesis technologies that can consider such examples of user intent as input to the synthesis of security specifications. Aspire combines such inputs, along with a domain specific language for security applications, to synthesize a candidate set of possible outputs. The user can either choose a candidate output or provide more examples to guide the synthesis process. In this iterative fashion, the user can generate system specifications, policies, or properties. Aspire uses concepts from the domain of formal methods, machine learning, and programming languages to perform synthesis. Aspire is applicable to a variety of domains including web, mobile, and cloud applications. The output of Aspire's synthesis can either be used for analyzing security vulnerabilities, or for compilation and testing with real systems.
