Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)

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