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.