Automatically eliminating speculative leaks from cryptographic code with blade
Automatically eliminating speculative leaks from cryptographic code with blade
复制标题
DOI：
10.1145/3434330
复制
发表时间：
2020-05
影响因子：
--
通讯作者：
Marco Vassena;Craig Disselkoen;K. V. Gleissenthall;Sunjay Cauligi;Rami Gökhan Kici;Ranjit Jhala;D. Tullsen;D. Stefan
中科院分区：
文献类型：
--
作者：
Marco Vassena;Craig Disselkoen;K. V. Gleissenthall;Sunjay Cauligi;Rami Gökhan Kici;Ranjit Jhala;D. Tullsen;D. Stefan
我们介绍了刀片，这是一种自动有效地消除刀片的投机性泄漏的新方法。它们通过缓存泄露（下沉），而不是完全禁止推测。瞬态，即可能包含投机性的秘密，或者是稳定的，（2）禁止投机性泄漏，要求所有水槽表达式都稳定使用现有的架构机制来实施保护，并显示Blade的类型系统如何自动合成最小数量的保护措施以正确消除投机性泄漏在Cranelift WebAssembly编译器中实现刀片，并通过修复几个经过验证但脆弱的WebAssembly实现加密原始的方法来评估我们的方法。保护。
We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative execution, it suffices to cut the dataflow from expressions that speculatively introduce secrets (sources) to those that leak them through the cache (sinks), rather than prohibit speculation altogether. We formalize this insight in a static type system that (1) types each expression as either transient, i.e., possibly containing speculative secrets or as being stable, and (2) prohibits speculative leaks by requiring that all sink expressions are stable. Blade relies on a new abstract primitive, protect, to halt speculation at fine granularity. We formalize and implement protect using existing architectural mechanisms, and show how Blade’s type system can automatically synthesize a minimal number of protects to provably eliminate speculative leaks. We implement Blade in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation automatically, without user intervention, and efficiently even when using fences to implement protect.