SACRED-MA: Safe And seCure REmote Direct Memory Access

SACRED-MA：安全可靠的远程直接内存访问

基本信息

批准号：
EP/X037142/1
负责人：
Brijesh Dongol
金额：
$ 59.44万
依托单位：
University of Surrey
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2023
资助国家：
英国
起止时间：
2023 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FX037142%2F1
关键词：
SACRED MA Safe seCure REmote

项目摘要

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.

现代社会依赖于以不断增长的速度访问和传输大量数据。诸如Google投资诸如全球数据中心的技术巨头，例如Google Investment数十亿美元。复制的数据系统构成了所有云服务的骨干；提高其可靠性和性能会影响所有云和大数据服务。英国目前是欧洲最大的云市场，在2020年，云投资超过170亿英镑。为了满足我们对快速数据传输的不断增长的需求，RDMA（远程直接内存访问）技术可以通过直接访问机器访问（读/写入）来实现下一代基础架构，从而使另一台机器的内存在网络中。与传统的网络协议堆栈（例如TCP/IP）不同，启用RDMA的网络接口卡（NICS）可以绕过操作系统内核，因此ANS能够进行电线速度数据传输。自2000年代中期以来，RDMA技术已在超级计算集群中提供，但直到最近，由于其成本，直到最近仍然是消费者和企业系统的实验功能。但是，最近随着负担得起的NIC的可用性（例如，由我们的合作伙伴Nvidia开发的）发生了变化，现在可以构建挑战常规设计范式的分布式应用程序。例如，人们可以利用RDMA的额外吞吐量来支持并发的前端应用程序，从而超过当今使用的顺序状态机器复制服务。通过开发无线RDMA和RDMA超过6G的开发，已经转向消费级设备。要释放企业和消费者系统中RDMA的潜力，我们必须使程序员能够编写安全和安全的程序。但是，目前通过非正式的平坦文本手册[22]和示例记录了RDMA的行为，并进行了语义投票和模棱两可。 RDMA的编程模型知之甚少，并且不支持正式验证。由于RDMA可以直接写入远程计算机的内存，因此会带来重大风险。此外，RDMA编程本质上是挑战，因为它需要了解远程通信与本地计算之间的相互作用，即远程存储器如何与给定计算机的本地内存写入相互作用，这有可能导致数据竞赛并增加安全和安全错误的风险。