SACRED-MA: Safe And seCure REmote Direct Memory Access

现代社会依赖于以不断增长的速度访问和传输大量数据。像苹果这样的科技巨头每年在世界各地的数据中心投资数十亿美元。复制数据系统构成了所有云服务的主干；提高它们的可靠性和性能将影响所有云和大数据服务。英国目前是欧洲最大的云市场，到2020年云投资将超过170亿英镑。为了满足我们对快速数据传输不断增长的需求，RDMA（远程直接内存访问）技术通过允许一台机器通过网络直接访问（读/写）另一台机器的内存来实现下一代基础设施。与传统的网络协议栈（如TCP/IP）不同，支持rdma的网络接口卡（nic）可以绕过操作系统内核，因此能够进行线速数据传输。自2000年代中期以来，RDMA技术已经在超级计算集群中可用，但由于其成本问题，直到最近在消费者和企业系统中仍然是一个实验性特性。然而，这种情况最近随着可负担得起的网卡（例如由我们的合作伙伴NVIDIA开发的网卡）的可用性而改变，现在可以构建挑战传统设计范例的分布式应用程序。例如，可以利用RDMA的额外吞吐量来支持并发前端应用程序，超越目前使用的顺序状态机复制服务。通过无线RDMA和超过6G的RDMA的发展，已经有了向消费级设备的转变。为了在企业和消费者系统中释放RDMA的潜力，我们必须使程序员能够编写安全可靠的程序。然而，RDMA行为目前是通过非正式的纯文本手册[22]和示例进行记录的，这使得它的语义模糊和模棱两可。人们对RDMA的编程模型理解得很差，并且不支持形式验证。这有很大的风险，因为RDMA支持直接写入远程机器的内存。此外，RDMA编程本身就具有挑战性，因为它需要理解远程通信和本地计算之间的交互，即远程内存写入如何与给定机器的本地内存写入交互，这可能导致数据竞争并增加安全性和安全性错误的风险。

Modern society depends on accessing and transferring vast quantities of data, at ever-increasing speeds. Technology giants such as Google invest billions of dollars every year into data centres across the world. Replicated data systems form the backbone of all cloud services; improving their reliability and performance impacts all cloud and big data services. The UK is currently the largest cloud market in Europe, with over £17 billion in cloud investment in 2020.To meet our ever-growing need for rapid data transfer, RDMA (remote direct memory access) technologies enable next-generation infrastructures by allowing a machine to access (read/write) directly the memory of another machine across a network. Unlike traditional network protocol stacks such as TCP/IP, RDMA-enabled network interface cards (NICs) can bypass' an operating system kernel, ans are thus capable of wire-speed data transmission. RDMA technology has been available in supercomputing clusters since the mid 2000s, but had until recently remained an experimental feature in consumer and enterprise systems due to its cost. However, this changed recently with the availability of affordable NICs (e.g. those developed by our partner NVIDIA), and it is now possible to build distributed applications that challenge conventional design paradigms. For instance, one can leverage the additional throughput of RDMA to support concurrent front-end applications, surpassing sequential state-machine replication services used today. There is already a shift towards consumer-grade devices through the development of wireless RDMA and RDMA over 6G.To unlock the potential of RDMA in enterprise and consumer systems, we must enable programmers to write safe and secure programs. However, the RDMA behaviour is currently documented through informal plain-text manuals [22] and examples, making its semantics vague and ambiguous. The programming models for RDMA are poorly understood, and there is no support for formal verification. This carries significant risks since RDMA enables writing directly into the memory of a remote machine. Moreover, RDMA programming is inherently challenging as it requires an understanding of the interaction between remote communication and local computation, i.e. how remote memory writes interact with the local memory writes of a given machine, potentially leading to data races and increasing the risk of safety and security bugs.