TRUSTED: SecuriTy SummaRies for SecUre SofTwarE Development

开源软件开发已经成为一种日益流行的做法。今天的软件系统由第一方代码和第三方依赖项组成，这些依赖项通过涉及不同个人、组织和工具的复杂供应链流程构建。攻击者通过故意将漏洞合并到要在软件生命周期的较后阶段触发的代码中，可以危害该过程中的任何步骤。最近对SolarWinds或Log4j漏洞的有影响力的攻击就是许多此类快速增加的攻击的例子。在这个项目中，我们将为提供可证明安全的开源软件奠定基础，并证明它是安全的。信息流控制是一种众所周知的机制，用于推理机密性和完整性。安全属性声明没有非法信息流，例如，没有秘密数据泄露到公共渠道，或者没有被污染的数据被传递到敏感的接收器。我们引入了安全摘要的概念，它说明了何时使用构件是安全的(即，没有非法流)，以及使用构件对安全相关行为的影响是什么。安全摘要是假设-保证推理的概念简单形式，有两个关键成分：(1)警卫，列出使用软件是安全的条件；(2)效果，表达使用软件的(安全)后果。虽然概念很简单，但实现它并不简单：较小的问题是，我们想要推理的软件可能包含数千行代码，而更大的问题是，它将依赖于拥有数千个概念的库的使用，这些库具有数百万行代码和复杂的相互作用。问题更多的是“从哪里开始？”而不是“如何继续？”，除非我们准备受制于毫无意义的玩具问题。我们将通过利用基于摘要的推理的组成特征来解决这个问题。方法调用的安全摘要是建立依赖它们的方法的安全摘要的关键。通过这种方式，我们可以将关于大型应用程序安全性的推理问题归结为关于单个小方法的安全性推理的较小问题，并将它们的结果合成以建立大型应用程序的安全性。虽然这使得软件只相对于这样的假设可靠，但它允许用证书(即正确的安全摘要)连续替换假设，或者用经过认证的方法替换未经认证的方法。一旦这一过程全面展开，经过认证的库将成为开源软件开发的宝贵资产，这将纯粹因为它们相对于未经认证的库所提供的竞争优势而存在。我们开发的方法将允许自动生成正确的安全摘要并透明地发布它们，这样代码消费者将能够在重用代码之前检查和验证代码的安全性，并检测供应链上的任何不当行为。安全摘要还带来了许多研究挑战。例如，方法可能带有一定程度的不确定性，这种不确定性的所有解决方案不一定都满足所需的安全保证--但我们需要找到一个确实满足的解决方案。类似地，虽然从安全摘要到被调用方法到总体所需属性的路径是明确的，但相反的方式(从我们的总体目标到对被调用方法的要求)提供了回旋余地。我们将提出尖锐的要求，这将使更新或替换调用的方法变得更容易，因为它的替换方法必须满足的要求有所放宽。解决这些问题使我们能够将有趣的理论挑战与实践相关性结合起来，这将有助于生产未来的安全系统。

Open-source software development has become an increasingly popular practice. Today's software systems comprise first-party code and third-party dependencies built through a complex supply chain process involving different individuals, organizations, and tools. An attacker can compromise any step in the process by deliberately incorporating vulnerabilities into the code to be triggered at a later stage of the software life cycle. The recent impactful attacks on SolarWinds or Log4j vulnerability are examples of many such rapidly-increasing attacks. In this project, we will lay the foundations of providing provably-secure open-source software - and to prove that it is secure.Information-flow control is a well-known mechanism to reason about confidentiality and integrity. A security property states that there is no illegal information flow, e.g., no secret data is leaked to public channels or no tainted data is ever passed to sensitive sinks. We introduce the concept of security summary, which states when it is secure to use an artifact (i.e., there is no illegal flow) and what are the effects of using the artifact on the security-related behaviour. Security summaries are a conceptually simple form of assume-guarantee reasoning with two key ingredients: (1) a guard, which lists conditions under which using the software is secure, and(2) an effect, which expresses the (security) consequences of using it.While the concept is simple, implementing it is not: the smaller problem is that the software we want to reason about may contain thousands of lines of code, while the larger problem is that it will rely on the use of libraries that have thousands of concepts with millions of lines of code and intricate interplay. The question is more "where to start?" than "how to proceed?", unless we are prepared to be constrained to meaningless toy problems. We will address this question by exploiting the compositional character of summary-based reasoning. Security summaries of methods calls are key to establishing the security summaries of methods that rely on them. In this way, we can reduce the problem of reasoning about the security of a large application into the smaller problems of reasoning about the security of individual small methods and compose their results to establish the security of a large application.It is quite possible to make security assumptions and then trust them. While this makes software reliable only relative to such assumptions, it allows for successively replacing assumptions with certificates (i.e., correct security summaries), or uncertified methods by certified ones. Once such a process is in full swing, certified libraries will become valuable assets for open-source software development, which will bring them into existence purely by the competitive advantage they provide over uncertified ones.The methods we develop will allow for automatically producing correct security summaries and transparently releasing them, so that the code consumer will be able to check and validate the security of a code before reusing it, and also detect any misbehaviour along the supply chain.Security summaries also hold many research challenges. For example, methods may come with a certain degree of nondeterminism, and it is not necessary that all resolutions of this nondeterminism satisfy the desired security guarantees - but we need to find one that does. Similarly, while the pathway from security summaries from called methods to the overall desired property is clear, the reverse way (from our overall goals to requirements on the methods called) provides leeway. We will deliver sharp requirements, which will make it easier to update or replace the method called, because the requirements its replacement has to fulfill are relaxed.Tackling these problems allows us to combine interesting theoretical challenges with practical relevance, that will help produce tomorrow's secure systems.