A Fast and Verified Software Stack for Secure Function Evaluation
A Fast and Verified Software Stack for Secure Function Evaluation
复制标题
用于安全功能评估的快速且经过验证的软件堆栈
DOI：
10.1145/3133956.3134017
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Almeida J
中科院分区：
文献类型：
--
作者：
Almeida J
我们提出了一个高保证的软件栈安全功能评估（SFE）。我们的堆栈由三个组件组成：i.将C程序翻译成布尔电路的经验证的编译器（CircGen）; ii.基于乱码电路和不经意传输的Yao的SFE协议的验证实现;以及iii.通过FRESCO实现透明的应用程序集成和通信，FRESCO是一个用于安全多方计算（MPC）的开源框架。CircGen是一个通用工具，它建立在CompCert之上，CompCert是一个经过验证的C优化编译器。它可以用于任意基于布尔电路的加密部署。我们的SFE协议实现的安全性使用EasyCrypt进行了形式化验证，EasyCrypt是一种用于构建高置信度加密证明的工具辅助框架，它利用了基于Bellare，Hoang和Rogaway框架的新的混淆电路形式化（CCS 2012）。我们对我们的方法进行了实际评估，并得出结论，它与最先进的（未经验证的）方法具有竞争力。我们的工作提供了具体的证据的可行性，建立高效的，验证，实现更高层次的密码系统。我们所有的发展都是公开的。
We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.
登录
查看更多内容
DOI：
10.1007/978-3-642-22792-9_5
发表时间：
2011-08
期刊：
--
影响因子：
--
作者：
G. Barthe;B. Grégoire;S. Heraud;Santiago Zanella-Béguelin
通讯作者：
G. Barthe;B. Grégoire;S. Heraud;Santiago Zanella-Béguelin
经过验证的计算安全协议规范的实现生成
DOI：
--
发表时间：
2013
期刊：
Journal of computing and security
影响因子：
--
作者：
David Cadé;B. Blanchet
通讯作者：
B. Blanchet
CBMC-GC：用于安全两方计算的 ANSI C 编译器
DOI：
--
发表时间：
2014
期刊：
International Conference on Compiler Construction
影响因子：
--
作者：
M. Franz;Andreas Holzer;S. Katzenbeisser;C. Schallhart;H. Veith
通讯作者：
H. Veith
SCAPI：安全计算应用程序编程接口
DOI：
--
发表时间：
2012
期刊：
IACR Cryptology ePrint Archive
影响因子：
--
作者：
Yael Ejgenberg;Moriya Farbstein;Meital Levy;Yehuda Lindell
通讯作者：
Yehuda Lindell
针对活跃对手的安全多方计算协议的隐私自动证明
DOI：
--
发表时间：
2015
期刊：
IEEE Computer Security Foundations Symposium
影响因子：
--
作者：
Martin Pettai;Peeter Laud
通讯作者：
Peeter Laud