没有合适的资源?快使用搜索试试~ 我知道了~
50综合安全有效的包处理1,Michael D.Wong2,Tanvi Wagle1,Srinivas Narayana1,Anirudh Sivaraman31罗格斯大学2普林斯顿大学3纽约大学k2_compiler@email.rutgers.edu摘要扩展Berkeley包过滤器(BPF)已经成为Linux操作系统中扩展包处理功能的一种强大方法 BPF允许用户用高级语言(如C或Rust)编写代码,并在内核中的特定钩子(如网络设备驱动程序)上执行它们。为了确保用户开发的BPF程序在内核环境中的安全执行,Linux使用了内核静态检查器。检查器允许程序执行,只有当它可以证明程序是无崩溃的,总是在安全范围内访问内存,并避免泄漏内核数据。BPF编程并不容易。第一,即使是中等大小的BPF程序被认为太大,分析和拒绝的内核检查器。第二,内核检查器可能会错误地确定BPF程序表现出不安全的行为。三,甚至是对BPF代码的小性能优化(例如, 5%的收益)必须由专家开发人员精心手工制作。传统的BPF优化编译器往往是不够的,因为内核检查器我们提出了K2,一个基于程序合成的编译器,自动优化BPF字节码与形式的正确性和安全保证。 K2产生的代码大小减少了6 -26%,平均包处理延迟降低了1.36%-55.03%,相对于最好的clang编译程序,吞吐量(每个核心每秒的数据包)提高了0-4.75%,这些基准来自Cilium,Facebook和Linux内核。 K2结合了几个特定领域的技术,通过加速合成,BPF程序的等价性检查提高了6个数量级CCS概念• 网络→可编程网络。关键词端点包处理,BPF,综合,随机优化ACM参考格式:作 者 : Michael D. Wong , Tanvi Wagle , Srinivas Narayana , andAnirudh Sivaraman. 2021年为数据包处理合成安全有效的内核扩展。 在ACM SIGCOMM 2021会议(SIGCOMM '21),2021年8月23日至28日,虚拟 活 动 , 美 国 。 ACM , 纽 约 州 纽 约 市 , 美 国 , 24 页 。https://doi.org/10.1145/3452296.3472929允许制作本作品的全部或部分数字或硬拷贝供个人或课堂使用,无需付费,前提是复制品不以营利或商业利益为目的制作或分发,并且复制品在第一页上带有此通知和完整的引用。必须尊重作者以外的其他人所拥有的本作品组件的版权。允许用信用进行提取 复制,或重新发布,张贴在服务器上或重新分发到列表,需要事先特定的许可和/或费用。 请求权限请发邮件至permissions@acm.org。SIGCOMM1引言考虑到来自大规模应用程序的数据量不断增加、摩尔定律停滞不前、云计算中CPU核心的货币化以及高端应用程序严格的吞吐量和延迟要求,服务器处理数据包的CPU效率至关重要网络社区已经做出了一些努力,包括操作系统包处理方面的创新[53,58,81,126],用户空间堆栈[45,47,64,87,105,117,123],以及可编程NIC卸载[15、22、24、25、74、76]。最近,扩展的Berkeley包过滤器(BPF)已经成为一种流行的方法,以实现灵活和高速的数据包处理在Linux操作系统上BPF起源于90年代早期的数据包过滤[107],后来演变成一个通用的内核虚拟机[59,83],具有表达性的64位RISC指令集。 BPF代码1已被广泛部署在生产系统中-实现负载平衡[56,131],DDoS保护[71],容器策略实施[90],应用程序级加密[21],入侵检测[70]和低级系统监控[42,80]。发送到Facebook [131]和Cloud-Flare[71]的每个数据包都由BPF软件处理。BPF使用户能够扩展操作系统的功能,而无需开发内核软件[79]。 用户以高级语言(例如,C,Rust),并使用标准编译器工具链(例如,Clang-9)生成BPF字节码。操作系统利用内核中的静态检查器,该检查器分析BPF字节码以确定在内核上下文中运行是否安全具体来说,检查器试图证明程序终止,不崩溃,不访问内核内存超出安全允许的界限,并没有泄漏特权内核数据。如果程序被内核检查器证明是安全的,它将被下载到内核内存中,并在没有任何额外的运行时检查的情况下运行否则,程序将被拒绝。BPF程序可以在包处理栈[104]的几个性能关键部分中执行,如网络设备驱动程序[83],流量控制[54],拥塞控制[92]和套接字过滤器[107]。BPF在灵活性、安全性和性能的结合方面是独一无二的,它使数据包处理成为可能。与可能使内核崩溃或损坏内核内存的内核模块不同,被内核检查器接受的BPF程序被保证不会行为不当,假设检查器和BPF运行时没有错误。与内核旁路堆栈不同,BPF不固定CPU内核,并保留用户-内核权限分离和标准管理工具(例如, tcpdump)在操作系统上可用[83,124]。尽管BPF的承诺,这是不容易的开发高质量的数据包处理代码在BPF今天。我们概述了三个挑战。©2021版权归所有者/作者所有。出版权授权给ACM。ACM ISBN 978-1-4503-8383-7/21/08。- 是的- 是的十五块https://doi.org/10.1145/3452296.34729291在本文中,我们使用术语BPF来表示BPF的扩展版本,而不是用于编写包过滤器的“经典”BPF。51SIGCOMM挑战1:性能。今天,优化BPF代码的性能就相当于优化汇编代码。用户空间分析工具尚未成熟[93]。编译器中的优化支持不足。 对于我们测试的基准测试,标准编译工具链(基于Clang-9)在优化标志-O2和-O3下生成相同的代码,错过了优化-O2代码的机会(第8节)。有趣的是,众所周知,即使是专家开发人员也必须付出艰苦的工作来提高BPF代码的性能[49,91,122]。然而,小的改进是值得的:考虑到可用于处理每个数据包的CPU时钟周期预算有限,每个数据包减少几个时钟周期对于满足高速线路速率至关重要[23,72,83]。此外,削减网络的CPU使用量减少了对同一台机器上共同托管的工作负载的干扰[37,97]。挑战2:规模。 运行超过适度大小的BPF程序会带来挑战。 内核检查器限制它认为可以接受的程序的复杂度2 [27,88],以保持加载用户程序所需的时间较小。在实践中,即使只有几千条指令的程序最终也会被拒绝[29]。此外,支持BPF卸载的硬件平台对程序大小非常敏感,因为它们的快速存储器数量有限,无法容纳程序[122]。 对代码压缩的更好的支持是有缺陷的:对于我们的大多数基准测试,我们发现clang-Os产生的代码大小与clang-O2相同。在规模压力下,开发人员唯一的办法就是重构他们的程序[3,10,28]。挑战三:安全。即使是小程序也很难通过内核检查。检查器的静态分析是不完整和不精确的:它拒绝了许多程序,这些程序具有可以接受的语义等价重写(§6)。 这使得开发产生可运行BPF字节码的编译器变得很棘手。Clang的BPF后端的开发人员专门致力于产生内核检查器将接受的指令序列,例如,[14、16- 19 ]。在设计gcc编译器的BPF后端时,产生检查器可接受的代码是一个主要挑战[60,67]。从根本上说,生成优化的、紧凑的和安全的BPF代码是具有挑战性的,因为检查器强制的安全限制和基于规则的优化之间不兼容(§2.2)。我们称之为BPF编译中的阶段排序问题:生成安全的、检查器可接受的代码排除了许多传统的基于规则的优化。相反,应用优化会产生内核检查器拒绝的代码。基于合成的编译器。 我们提出K2,一个编译器,它使用程序合成自动生成安全,紧凑,高性能的BPF字节码,从未优化的字节码。 程序综合是寻找一个满足给定规范的程序的任务[38]. 规范的一个例子是,合成程序的输出必须与源程序的所有输入相匹配。合成的工作原理是在空间中搜索2旧的内核(v5.2之前)拒绝超过4096 BPF字节码指令的程序。在现代内核中,这个限制仍然适用于非特权BPF程序类型[34],例如套接字过滤器和容器级包过滤器[35]。从内核v5.2开始,检查器的静态分析检查的指令数量限制为100万[13,34],这是一种带有修剪算法的符号执行形式[ 57 ]。不幸的是,被检查的指令的数量随着程序中的分支而迅速爆炸,导致许多甚至小于4096条指令的程序由于这个限制而被拒绝[30 -33,36]。通常由用户提供的对合成程序的结构的限制来引导。例如,合成器可以搜索适合用户定义语法的程序[132,133],使用较小的库组件[82,89],或使用低级指令集[41,113,118,127]。虽然传统的编译器被设计为在很小的时间预算内发出 我们相信,对于BPF程序来说,更长的编译时间是值得的,因为它们在部署的系统中很流行,它们对性能很敏感,即使实现很小的性能增益也很困难,而且它们在机器和架构上的可移植性[20,114]。K2有三个贡献。贡献1:BPF的随机合成(§3)。 K2使sto-随机合成[55,128,130]适应BPF指令集的域。在高层次上,该算法运行马尔可夫链来搜索具有较小成本函数值的程序,该成本函数包含正确性,安全性和性能。一个新的候选程序合成概率使用修改马尔可夫链的当前状态(程序)的几个重写规则之一马尔可夫链以与相对于当前程序的成本减少成比例的概率转换到新状态(合成程序)。我们将展示如何设置K2来优化安全约束下具有不同成本函数的程序。我们已经整合了几个特定领域的重写,以加速搜索。 在搜索结束时,K2产生同一输入程序的多个优化版本。贡献2:BPF程序的等价性检查技术(§4,§5)。K2合成的程序在形式上被证明是等价于原始程序。为了执行等价性检查,我们用一阶逻辑形式化了BPF程序的输入输出行为(§4)。我们的形式化包括BPF的算术和逻辑指令,这些指令由BPF的早期处理[77,115,116,138]处理,并且通过合并别名内存访问(使用指针)以及BPF映射和帮助函数(§2)超越了先前的工作。等效性检查发生在合成的内部循环中,并且它必须是有效的以使合成保持实用。我们提出了几种特定领域的技术,可以将检查两个BPF程序的输入输出等效性所需的时间减少五个数量级(§5)。因此,K2可以优化生产系统中使用的实际BPF代码。贡献3:检查BPF程序安全性的技术(§6)。 在随机搜索的每一步,K2评估候选程序的安全性。 K2包含了对程序控制流和内存访问的安全检查,以及几个内核检查器特定的约束。为了实现这些检查,K2采用静态分析并释放在候选程序上写入的一阶逻辑查询。K2通过在搜索的每一步都考虑候选程序的性能和安全性,解决了BPF编译的阶段排序问题。 虽然K2的安全检查与内核检查器的安全检查有很大的重叠,但这两组检查是不同的,因为内核检查器是一个正在积极开发的复杂代码体[ 26 ]。有可能,虽然不太可能,综合安全有效的包处理内核扩展SIGCOMM52K2认为一个程序是安全的,但内核检查器拒绝了它。为了保证K2的输出是内核检查器可以接受的,K2有一个后处理过程,它将每个最好的输出程序加载到内核中,并清除任何未通过内核检查器的程序。 虽然这个过程的存在可能会带来阶段排序问题,但它只是一个故障安全:在撰写本文时,所有K2的搜索输出程序都已经通过了内核检查器。K2可以使用clang发出的BPF对象文件,并生成一个优化的、直接的替换。 我们提出了一个评估的编译器从Linux内核,纤毛,和Facebook绘制的19个程序。 相对于最好的clang编译变体(在-O2/-O3/-O中),K2可以将BPF程序的大小减少6 - 26%,将平均延迟减少1.36%-55.03%,并将吞吐量(以每个核心每秒的数据包为单位)提高0- 4.75%。 这是与需要专家开发人员做出重大努力才能产生5-10%性能增益的现有技术相比[91,131]。K2是一个存在的证明,特定领域的应用程序的gram合成技术是一个可行的方法来自动优化性能关键的数据包处理代码。我们呼吁社区探索这种技术,以减轻开发人员在用户空间网络和可编程以太网等其他环境中提高性能的负担。 K2https://k2.cs.rutgers.edu/。2背景和动机2.1扩展Berkeley包过滤器BPF是一个通用的内核虚拟机和指令集[59],使用户能够为Linux编写操作系统扩展[79]。 标准编译器(例如,Clang-9)可以用来将C/Rust程序转换为BPF字节码,其格式与底层硬件架构无关。BPF程序是事件驱动的。 BPF字节码可以附加到操作系统中的特定事件,例如数据包到达网络设备驱动程序[83],Linux流量控制中的数据包入队[95],拥塞控制处理[92]和套接字系统调用调用[104]。使用BPF帮助函数支持有状态功能。Helper函数作为内核的一部分实现,可以由BPF程序使用适当的参数调用。例如,有一些帮助函数提供对持久键值存储(称为映射)的访问。与地图相关的帮助函数包括查找、更新和删除。映射帮助器的参数包括指向内存的指针和唯一标识映射的文件描述符。内核中的助手列表和功能都在稳步增加;截至本文撰写时,最新的内核中有超过100个助手[96]。BPF指令集遵循64位RISC架构。 每个程序可以访问11个64位寄存器、大小为512字节的程序堆栈(由堆栈指针寄存器r10引用),以及访问包含程序输入(诸如分组)和一些内核数据结构(例如,套接字缓冲器)。 BPF指令集包括32位和64位算术和逻辑运算、有符号和无符号运算以及基于指针的加载和存储指令。BPF程序可以通过利用即时(just-in-time)来高效地执行BPF并不打算成为图灵完备语言;它不支持执行无限循环。用户提供的BPF程序直接在内核上下文中运行。为了确保这样做是安全的,Linux利用了内核中的静态检查器。2.2带通滤波器的相位排序我们说明了为什么它是具有挑战性的,以优化BPF字节码,同时满足内核检查器执行的安全约束。这些示例来自我们在内核v5.4中对检查器的实验。 在下面的程序中,我们使用r0... r9用于通用BPF寄存器。R10保存堆栈指针。例1.无效的强度降低。 序列bpf_mov rY 0// rY = 0bpf_stx rX rY// *rX = rY对于某些寄存器,rX和rY通常可以优化为更简单的单指令bpf_st_imm rX 0// *rX = 0然而,内核检查器要求指向程序的“上下文内存”的指针如果rX是这样一个指针,程序将被拒绝。实施例2.内存访问合并无效 考虑指令序列bpf_st_imm8 rX off1 0// *(u8*)(rX + off1)= 0bpf_st_imm8 rX off2 0// *(u8*)(rX + off2)= 0其中rX是可安全访问的存储器地址,并且off1和off2是偏移,使得off2=off1+1。通常,两个这样的1字节写入可以组合成一个2字节写入:bpf_st_imm16 rX off1 0// *(u16*)(rX + off1)= 0然而,内核检查器要求堆栈中的存储必须与相应的写入大小对齐[8]。 如果rX是堆栈指针r10,并且off1不是2字节对齐的,则检查器将拒绝重写的程序。一般来说,应用通过检查器约束的优化检查器有许多限制[5,6],使得考虑优化和安全条件的叉积变得繁琐。2.3K2:一个基于程序综合的编译器K2是一个利用程序综合来综合考虑程序正确性、性能和安全性的编译器而不是零敲碎打,以解决BPF优化中效率和安全性之间程序综合是寻找满足给定规范的程序的组合搜索问题 附录A概述了文献中的程序综合方法。 给定一个BPF字节码格式的指令序列,我们有兴趣合成一个备选的BPF指令序列,它满足以下规范:(i)合成程序在输入输出行为上与源程序等效,(ii)合成程序是安全的,(iii)合成程序是更有效的SIGCOMM徐琼文等53psrcK2p电p下p合成输入失通过测试用例失加计数器通过或失败等效、安全、性能最佳的程序程序解释器(§7)确定下一步状态psynth或pcurr(§3.3)设置当前状态提案生成(§3.1)clang编译的BPF目标文件优化BPF字节码等效性(§4,§5)()(·)(→)安全标准(§6)例通过成本函数(§3.2)总成本图1:K2编译器的概述。实线箭头表示控制流虚线箭头表示数据流比源程序。有效性和安全性的精确定义将在§3和§6中讨论。图1介绍了K2的概述,它综合了满足上述规范的 K2消耗Clang编译的BPF字节码,并实现§3中描述的随机搜索过程。 搜索过程综合提议,这些提议是字节码的候选重写。 该建议是根据一套自动生成的测试用例进行评估,以快速修剪程序不等同于源程序,或不安全。如果提案通过了所有测试,K2使用形式等价性检查(§4,§5)和形式安全性检查(§6)来确定提案的成本函数值成本结合了正确性、安全性和性能特征,并用于引导搜索过程朝向更好的程序。 形式等价性检查和安全性检查可能会产生反例,即。输入,其中建议的输出与原始字节码的输出不同,或者建议表现出不安全的这些测试被添加到测试套件中,以便在将来快速修剪类似的程序。 我们描述了编译器实现的各个方面,包括我们在第7节中开发的BPF程序解释器。3带通滤波器的随机优化K2编译器将程序从BPF字节码转换为BPF字节码。K2使用STOKE [ 128 ]中介绍的随机优化框架,该框架应用马尔可夫链蒙特卡罗(MCMC)采样方法来优化程序空间上的成本函数。在高层次上,MCMC是一种从状态的概率分布中对状态进行采样的方法当我们将MCMC应用于程序优化时,状态是一个固定大小的程序 著名的MCMC采样器,Metropolis-Hastings(MH)算法[78],工作如下。 从一个初始状态开始,在每一步中,该算法使用状态之间的转移概率(§3.1)提出一个要转移到的新状态。该算法计算提议的成本函数(§3.2),并根据成本决定是接受还是拒绝提议的新状态(§3.3)。如果如果该状态被接受,则该状态成为马尔可夫链的新状态。 如果不是,则当前状态是马尔可夫链的新状态。 在渐近极限中,在转移概率的温和条件下[78],所有可接受状态的集合形成稳态概率分布的代表性样本。为什么是随机合成?在文献(附录A)中的程序综合方法中,K2主要采用随机搜索,因为它可以优化复杂的成本函数,例如,在程序执行过程中的高速缓存未命中的数量,具有复杂的约束条件,即,安全性。 MCMC使用标准转换将非常一般的成本函数(§3.2)转换为稳态概率分布,使其能够通过从相应的分布[73,78,128]中采样来执行优化。3.1提案生成马尔可夫链首先将其初始状态设置为输入程序p src。 从任何当前状态p_curr开始,我们生成候选重写,即使用以下规则之一,以固定概率prob随机选择的建议psyn。 :(1) 换一个指令(probir):随机选择一个指令,结构,并修改其操作码和操作数。例如,将bpf_add r1 4更改为bpf_mov r4 r2。(2) 替换一个操作数(probor):随机选择一个指令,并将其中一个操作数替换为相同类型的另一个值。例如,将bpf_add r1 4更改为bpf_add r1 10。(3) Replace by NOP(probnr):随机选择一条指令,然后用nop替换它,有效地减少了程序中的指令数量(4) 交换内存类型1(probme1):随机选择一条指令,如果是基于内存的指令(即加载或存储),对存储器操作的新宽度和新的立即数或寄存器操作数进行采样。指令的内存地址操作数(即地址基址和偏移量)以及其类型(加载与商店)不变。例如,更改r1 =* (u16*)(r2 - 4)至r3 = *(u32*)(r2 - 4)。(5) 交换内存类型2(问题2):随机选择一条指令,如果是基于内存的指令,则为内存操作采样一个新的宽度。所有其他指令操作数不变。例如,更改r1 =*(u16*)(r2- 4)到r1 = *(u32*)(r2 - 4)。(6) 替换连续指令(probcir):随机选择k个连续指令(我们选择k=2),并将它们全部替换为新指令。这些重写规则定义了马尔可夫链的转移概率,我们用trpcurrpsynth表示。我们使用表8(附录F.1)所示的概率prob根据我们的经验,任何允许马尔可夫链在程序空间中“自由”移动的概率都重写规则的非正交性 上述重写规则在它们影响的程序修改中并不互斥。例如,用NOP替换(规则3)只是更通用的指令替换(规则1)的特定版本只要有足够的时间,一小部分通用规则就足以探索程序的空间。然而,更具体的规则的存在加速了马尔可夫链收敛到更好的程序。综合安全有效的包处理内核扩展SIGCOMM54()()()()∈()()| |/||()()•()•()()srcsynth()(−)()..Σ()在所有的输入。我们想要一个函数,它提供了一个光滑的测量程序p相对于源代码的正确exec(isynth)−isrc∈psrcexec(isrc).重写规则的领域特异性。STOKE及其变体[55,128]提出了上述重写规则(1 -3)的变体。 规则(4)、(5)和(6)是K2用来加速搜索更好的BPF程序的特定于域的规则。 规则(4)和(5)有助于识别基于内存的代码优化(§9)。规则(6)捕获多个指令的一次性替换,例如,将后面跟着存储的寄存器加法替换为单个存储器加法指令。这些特定于域的规则既提高了结果程序的质量,又缩短了找到更好程序的时间(第8节,附录F.1)。3.2成本函数我们计算每个候选程序的成本函数成本函数f p包含三个分量:错误成本、性能成本和安全成本。错误成本。当且仅当程序p产生与源程序psrc相同的输出时,误差成本函数err p为0考虑来自等式(1)的所有变型,存在8个误差成本函数。 我们用每个成本函数并行运行MCMC,并返回所有成本函数中性能最好的程序。性能成本。我们使用两种性能代价对应于不同的场景,即优化程序的大小和程序的性能。函数per finst psynth(指令计数)是psynth中相对于psrc的额外指令数。函数per flat psynth是执行程序psynth相对于psrc的附加等待时间的估计。不幸的是,执行候选BPF程序psynth来直接测量其延迟是不可行的,因为内核检查器将拒绝大多数可以执行的程序。didate程序。相反,我们通过在轻负载系统上执行每个操作码数百万次,并确定每个操作码i的平均执行时间exec(i)来分析BPF指令集的每个指令。性能成本函数是不同的。所有o pco的总和的nce。德拉韦岛e. ,perflat(psynth):=我sn nn∈psn nn程序Psrc,以引导搜索朝向 与STOKE类似,我们将测试用例和形式等价性检查(§4&§5)结合起来计算错误成本。使用一组测试T并对每个测试t T执行psynth,我们设置.安全成本。据我们所知,K2是第一个合成编译器,将一阶逻辑中的通用安全约束纳入综合。K2所考虑的安全特性见§6。 我们处理不安全程序的方法很简单:一旦程序psynth被认为 是 不 安 全 的 , 我 们 将 saf e psynth 设 置 为 一 个 大 值ERR_MAX,只留下一个小概率,()err(p):=c· t∈T diff(opsynth(t),opsrc(t))+(一)进入马尔可夫链。 我们设置saf e psynth = 0,安全方案。我们不只是拒绝不安全的程序,其中:unequal·num_tests从当前程序到更高性能和更安全的马尔可夫链中的一个程序可能会通过一个不安全的程序(关于为什么的一些直觉,请参见图2)。4 in [128])。我们离开制定opt和opt是测试用例t上的建议和源程序的输出,diffx,y是两个值之间距离的度量我们考虑两个变体:(i)diff popx,y:=popcountxy是x和y之间不同的比特数,以及(ii)diff_abs_x,y:= abs_x_y,其表示x和y之间的数值差的绝对值。 相对于仅将popcount视为值之间的语义距离的STOKE,我们还发现许多分组处理程序需要数值正确性(例如,计数器),通过diff abs捕获。- 是的c是表示每个测试的权重的归一化常数案子STOKE为每个测试用例添加完整的错误成本,设置c=cfull=1。我们还探索了第二个变体,cav <$=1T,其中T是测试用例的数量,以规范化我们需要修剪复杂的“几乎正确”的BPF程序的许多测试用例的贡献如果两个BPF程序的一阶逻辑形式化(§4)发现程序是等价的,则equal为0,否则为1. 我们只在所有测试用例都通过的情况下运行等价性检查,因为它很耗时。如果任何一个测试用例失败,我们设置不等于1。num_tests包括两个变量:(i)p产生不正确输出的测试用例的数量,以及(ii)p产生正确输出的测试用例的数量。STOKE只使用第一个变量。 我们认为第二个变种,以区分一个程序,这是等价的源程序,满足所有的测试用例,但不是等价的。平滑的成本函数,以引导搜索通过逐步我们使用的最终成本函数是αerr(psynth)+βperf(psynth)+γsafe(psynth)。 我们运行不同(α,β,γ)的并行马尔可夫链,并返回具有最小性能成本的程序。3.3提案接受为了确定候选提案是否应该被用作马尔可夫链的下一个状态,成本f psyn被转换为稳态分布中psyn的概率,如下所示[78]:π(psynth)=e−β·f(psynth)/Z(2)当Z=pe−β·f(p)。Metropolis-Hastings算法计算psyn的接受概率,如下所示:α=min1,π(psynth)·tr(psynth→pcurr)(3)π(pcurr)·tr(pcurr→psynth)对于概率α,马尔可夫链的下一个状态被设置为psyn,否则下一个状态就是pcurr。在这里,TR。是程序之间的转移概率(第3.1节)。直观地说,如果psynth的成本低于p curr的成本,那么它总是被接受的。否则,psynn被接受的概率随着psy nn相对于pcurr的成本的增加而减小。K2从新状态开始重复§3.1、§3.2和§3.3中的过程马尔可夫链,循环直到超时。···SIGCOMM徐琼文等55∧4BPF程序等价性的证明K2合成输出程序,这些输出程序在形式上被证明与输入程序等价为此,我们首先使用位向量理论,在一阶逻辑形式化两个程序的输入输出行为[99]。 我们根据它们所连接的内核钩子来识别这两个程序的输入和输出寄存器[88]。然后,我们将下面的逻辑查询分派给求解器:输入到程序1 ==输入到程序2∧程序1∧程序2⇒程序1的输出!程序2如果公式是可满足的,那么就有一个共同的输入导致两个程序的输出不同,这个输入被添加到测试套件中(§3)。 如果公式是不可满足的,则这两个程序在输入输出行为方面是等价的。本节的其余部分描述了我们如何在一阶逻辑中获得单个程序的输入输出行为我们的形式化处理算术和逻辑指令(§4.1),内存访问指令(§4.2),BPF映射和其他帮助函数(§4.3)。我们已经检查了我们的形式化的合理性,使用一个测试套件,比较输出的逻辑公式与执行给定输入的指令的结果。你是谁? 我们首先重新排序程序中的指令,以便所有控制流只向前移动。当BPF程序不包含任何循环时,可以这样做然后,我们将整个程序转换为静态单赋值(SSA)形式[39,63]。SSA转换后的结果是BPF字节码指令序列,其中(i)对寄存器的每次分配使用具有版本号的新标签,例如,bpf_mov r 0 1; bpf_mov r 0 2被转换为bpf_mov r0_v1 1; bpf_mov r0_v2 2,以及(ii)每个语句与定义良好的路径条件相关联[111]。例如,在指令序列中,bpf_jeq r1 0 1// if r1!=0:bpf_mov r2 1//r2 = 1第二条指令与路径条件r1!= 0. 在最高层次上,我们构造对应于每个指令的一阶公式,并将它们连接起来,即。通过逻辑合取运算符,产生一个表示整个程序的输入输出关系的最终公式。现在我们讨论K2如何形式化每种指令。4.1算术和逻辑指令为了对基于寄存器的算术和逻辑指令进行建模,我们使用64位宽的位向量数据类型来表示每个寄存器的每个版本。每个指令的动作通过表示其对所有相关寄存器的影响来形式化我们的形式化处理32位和64位操作码,以及数据的有符号和无符号解释。例如,考虑32位算术指令bpf_add32dst src(操作码0x04),其具有采取寄存器dst和src的最低有效32位、将它们相加并将(可能截断的)32位结果写回dst、将dst寄存器的最高有效32位置零假设我们有一条指令bpf_add32 dst_x src_y(在SSA之后),其中x和y分别表示dst和src的版本号假设结果存储在dst_z中。此指令将导致公式(tmp==(dst_x.extract(31,0)+ src_y.extract(31,0)(dst_z == concat(bv32(0),临时提取物(31,0)其中TMP是用于保持DST_X和SRC_Y的32位相加的中间结果的新鲜变量,Extract(a,b)表示拾取位A.b,concat(x,y)表示通过连接两个位向量x和y而产生的位向量,其中x占据结果中的较高有效位,而bv32(0)是表示0的32位位向量类似地,我们已经构建了所有64位和32位算术和逻辑指令的语义表示[4]。4.2存储器访问指令BPF支持使用指针的不同大小的内存加载和存储指令[4 我们直接在位向量理论中对存储器操作进行编码,以在单个一阶理论中产生有效的编码。我们展示了这种编码如何在三个步骤中发生第1步:在没有任何存储的情况下处理负载假设一个BPF程序不包含存储器,只包含加载指令,即,bpf_ldrX rY。为了使描述简单,从这里开始,我们将使用符号rX =*rY来表示上面的指令编码负载中的关键挑战是处理混叠,即,不同的指针rY可能指向相同的存储器区域,因此不同的rX必须具有相同的值。假设在程序中遇到的第i个加载指令从存储器地址rY_i读取并加载到寄存器rX_i中。然后对于第i个载荷,我们结合公式j<$i(rY_j==rY_i<$rX_j==rX_i)公式化此公式需要维护程序中可能影响给定加载指令的所有先前加载为了实现这一点,K2为程序维护了一个内存读取表:每个加载的源和目的地都按照后SSA指令序列中出现的顺序添加到这个表K2通过将多字节加载扩展为多个单字节加载来处理加载地址中的部分重叠。步骤2:在直线程序中处理存储和加载 存储使上面的公式复杂化,因为形式为rX =*rY的加载必须捕获由rY指向的存储器的最新写入。例如,在指令序列rX_1 =*rY;*rY = 4; rX_2 =*rY中,来自rY的第一和第二加载可以返回要存储在rX_1和rX_2中的不同值。假设程序不包含分支。然后,对存储器地址的最新写入可以由写入相同地址的最近的存储指令(如果有的话)捕获(按照遇到的SSA指令的顺序)。 K2维护一个内存写表,它记录了内存地址和存储的变量,对应于ING在程序中的每个存储。假设k个存储器的形式为*rY_i= rX_i(ifrom1· · ·k)的问题56≤()⇒ ()()..从O((N))到O(N),其中N表示ttt的个数为数据包处理合成安全有效的内核扩展SIGCOMM'21,2021年8月23日至28日在加载指令之前,rX_l =*rY_l。然后,通过以下公式对载荷进行编码我们已经添加了用于获取随机数的帮助程序的形式化,访问当前的Unix时间戳,调整内存头-j:j<$≤ki:j<$i≤k!(rY_i ==rY_l)数据包缓冲区中的空间,并获取程序运行所在的处理器的IDrY_j ==rY_lrX_j ==rX_l公式i:j
下载后可阅读完整内容,剩余1页未读,立即下载
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)