Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)

计算硬件的持续发展已经导致具有集成高级存储器技术和硬件模型的执行模型的极其复杂的架构。这种演变影响到所有设备，从大型数据中心到移动的电话。然而，这些先进的架构打破了程序员所依赖的假设，导致了新的安全漏洞和安全漏洞。我们的目标是多处理器系统和并发体系结构，从而支持并发程序的开发。并发行为是出了名的困难--不正确的同步可能导致许多危险的安全和安全漏洞，从“越界写入”和“释放后使用”错误到“不正确的同步和竞争条件”。此外，基于架构的攻击（例如，这表明了解决这些问题的紧迫性。即使底层程序同步良好，底层并发算法的设计本身也可能是脆弱的。特别是，众所周知的安全条件，如线性化不能保证安全性，目前解决这个问题的方法会导致过度同步的实现（降低性能）。这在硬件设计者（旨在最大限度地提高性能）和最终用户（需要可靠软件）的目标之间引入了紧张关系。中间是开发人员，他们的任务是开发平衡这种紧张关系的软件。COVERT为可证明正确的可重用抽象提供了机制，最大限度地提高了程序设计的灵活性，允许基于架构对安全性和安全性保证进行微调。我们的愿景是提供（a）可重用的模型，工具和技术，使验证的安全性和安全属性的范围内的先进的体系结构，和（B）一组验证的并发抽象，保证安全和安全。这项工作涉及两个关键方面的工作。在第一个，我们汇集了现代系统的不同方面，并提供了一个严格的基础，涵盖了一系列的架构功能，如乱序执行和推测执行，以及内存功能，如弱内存和NVM。此外，我们通过开发威胁模型，将现有的推理技术扩展到我们新建立的基础之上，这些威胁模型通过恶意攻击者的透镜投射高级架构所允许的复杂行为。我们的第二条链涉及通过验证石蕊测试，验证并发库和相关的验证工具，这些技术的实际实现。我们将构建新的技术和工具，加强传统的正确性标准（线性化，不透明等），以提供安全和安全的架构感知的正确性。为了确保高度的可靠性，我们的理论和案例研究将在Isabelle证明助手中进行机械化。我们选择的案例研究包括来自MITRE数据库，Folly并发库以及我们的工业合作伙伴提供的示例。在学术传播方面，我们预计每个机构每年至少有2份期刊出版物，加上每年几次相关的会议出版物和主题演讲/特邀演讲。我们与标准化工作有着直接的联系，我们已经计算了持续参加标准会议的费用（例如，出席第1小组，并发，第21工作组，C++，在ISO -巴蒂是英国代表团的投票成员）以便我们的工作可以对相关的编程模型标准产生直接影响。通过我们更广泛的项目合作伙伴和我们现有的合作网络的参与，我们希望不仅增加了传播的机会，而且通过与这些更广泛的社区的互动，增加了我们的PDRA发展的机会。

The continuing evolution of computing hardware has led to enormously complex architectures with execution models that integrate advanced memory technologies and hardware models. This evolution affects all devices, ranging from large-scale data centres to mobile phones. However, these advanced architectures break assumptions that programmers have relied on, causing new safety bugs and security vulnerabilities. We target multi-processor systems and concurrent architectures, thus support the development of concurrent programs. Concurrent behaviour is notoriously difficult -- incorrect synchronisation can lead to many dangerous safety and security vulnerabilities, ranging from "out-of-bounds writes" and "use-after-free" errors to "improper synchronisation and race conditions". Further, architecture-based attacks (e.g., Spectre) show the urgency of addressing these important problems today. Even when low-level programs are well synchronised, the design of the underlying concurrent algorithms can themselves be vulnerable. In particular, well-understood safety conditions such as linearizability do not guarantee security, and current approaches to addressing this issue lead to overly synchronised implementations (degrading performance). This introduces a tension between the goals of the hardware designers (who aim to maximise performance), and end users (who require trustworthy software). In the middle are developers, who are tasked with producing software that balances this tension. COVERT provides mechanisms for provably correct reusable abstractions that maximise flexibility in program design, allowing fine-tuning of both safety and security guarantees based on the architecture. Our vision is to provide (a) reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures, and (b) a verified set of concurrency abstractions that guarantee both safety and security. This effort involves two key strands of work. In the first, we bring together different facets of modern systems and provide a rigorous foundation covering a range of architectural features such as out-of-order execution and speculative execution, and memory features such as weak memory and NVM. Additionally, we extend existing reasoning techniques above our newly established foundation by developing threat models that cast the intricate behaviours allowed by advanced architectures through the lens of a malicious attacker. Our second strand involves the practical realisation of these techniques via verified litmus tests, verified concurrency libraries and associated verification tools. We will build novel techniques and tools that strengthen traditional correctness criteria (linearizability, opacity etc) to provide architecture-aware correctness of both safety and security. To ensure a high degree of reliability, our theory and case studies will be mechanised within the Isabelle proof assistant.Our chosen case studies include those from the MITRE database, the Folly concurrency library as well as examples provided by our industrial partners. In terms of academic dissemination, we expect a minimum of 2 journal publications per year per institution, plus several associated conference publications and keynote / invited talks per year. We have a direct link to standardisation work, and we have costed in continued visits to standards meetings (eg attendance of Subgroup 1, concurrency, at Workgroup 21, C++, at the ISO - Batty is a voting member of the UK delegation) in order that our work can have a direct impact on the relevant programming model standards.By involvement of our wider project partners and our existing collaboration networks we expect not only enhanced opportunities for dissemination, but also enhanced opportunities for development of our PDRAs through interaction with these wider communities.