TWC: Medium: Collaborative: Aspire: Leveraging Automated Synthesis Technologies for Enhancing System Security

设计安全系统和验证现有系统的安全性是我们社会面临的严峻挑战。要实现安全的应用程序，一个严重的绊脚石在于为安全策略生成正确的系统规范。对于系统设计人员和最终用户来说，用形式逻辑来表达他们的意图都不是微不足道的。类似的挑战困扰着用户试图验证现有应用程序的安全属性，例如基于Web或云的服务，这些服务通常没有正式规范。因此，迫切需要能够弥合用户意图表达和系统规范之间差距的机制。这项研究设计了一种方法和一个名为Aspire的系统，能够将用户意图转换为安全规范。Aspire将用户意图的表达作为输入，例如系统演示、应用程序输入-输出示例或自然语言。ASPIRE利用了自动合成技术领域的最新发展，这些技术可以将用户意图的例子视为合成安全规范的投入。ASPIRE将这些输入与用于安全应用的领域特定语言相结合，以合成可能的输出的候选集合。用户可以选择候选输出或提供更多示例来指导合成过程。在这种迭代方式中，用户可以生成系统规范、策略或属性。ASPIRE使用形式化方法、机器学习和编程语言领域的概念来执行综合。Aspire适用于各种领域，包括Web、移动和云应用。Aspire合成的结果既可用于分析安全漏洞，也可用于编译和测试真实系统。

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.