TRUSTED: SecuriTy SummaRies for SecUre SofTwarE Development

值得信赖：安全软件开发的安全摘要

• 批准号: EP/X037274/1
• 负责人: Narges Khakpour
• 金额: $ 62.77万
• 依托单位: Newcastle University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FX037274%2F1
• 关键词: TRUSTED; SecuriTy; SummaRies; SecUre; SofTwarE

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.

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

项目成果

Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings

验证、模型检查和摘要解释 - 第 24 届国际会议，VMCAI 2023，美国马萨诸塞州波士顿，2023 年 1 月 16-17 日，会议记录

• DOI: 10.1007/978-3-031-24950-1_4
• 发表时间: 2023
• 作者: Berthier N