Developing secure distributed systems is difficult, and even harder when advanced cryptography must be used to achieve security goals. Following prior work, we advocate using secure program partitioning to synthesize cryptographic applications: instead of implementing a system of communicating processes, the programmer implements a centralized, sequential program, which is automatically compiled into a secure distributed version that uses cryptography. While this approach is promising, formal results for the security of such compilers are limited in scope. In particular, no security proof yet simultaneously addresses subtleties essential for robust, efficient applications: multiple cryptographic mechanisms, malicious corruption, and asynchronous communication. In this work, we develop a compiler security proof that handles these subtleties. Our proof relies on a novel unification of simulation-based security, information-flow control, choreographic programming, and sequentialization techniques for concurrent programs. While our proof targets hybrid protocols, which abstract cryptographic mechanisms as idealized functionalities, our approach offers a clear path toward leveraging Universal Composability to obtain end-to-end, modular security results with fully instantiated cryptographic mechanisms. Finally, following prior observations about simulation-based security, we prove that our result guarantees robust hyperproperty preservation, an important criterion for compiler correctness that preserves all source-level security properties in target programs.

翻译：开发安全的分布式系统十分困难，当必须使用高级加密技术来实现安全目标时尤为如此。借鉴先前工作，我们主张采用安全程序分区方法来合成加密应用：程序员无需实现通信进程系统，而是实现一个中心化、顺序化的程序，该程序会自动编译为使用加密技术的安全分布式版本。尽管这种思路前景可观，但相关编译器安全性的形式化结果仍局限于有限范围。特别是，目前尚无安全性证明能同时处理鲁棒高效应用所必需的关键细节：多重加密机制、恶意破坏和异步通信。在本工作中，我们开发了一种能处理上述细节的编译器安全性证明。该证明创新性地融合了基于模拟的安全性、信息流控制、编排编程以及并发程序的顺序化技术。虽然我们的证明针对的是将加密机制抽象为理想化功能的安全混合协议，但该方法为实现端到端模块化安全结果提供了清晰路径——通过利用通用可组合框架，可完全实例化加密机制。最后，基于先前对基于模拟安全性的观察，我们证明了该结果能保证鲁棒超属性保留，这是编译器正确性的重要准则，可确保目标程序中保留所有源级安全属性。