2016 · 79 citations · 33 references
EngineeringInformation SecurityCompiler TechnologyVerificationSoftware AnalysisFormal VerificationHardware SecuritySecure ComputingCompilersNew ResearchDynamic CompilationCompiler DesignSecure Multi-party ComputationRuntime VerificationCompiler SupportComputer EngineeringComputer ScienceOptimizing CompilerLanguage-based SecurityData SecurityCryptographyProgram AnalysisEfficient CompilerFormal MethodsSecure Computation
Recent developments in secure computation have led to significant improvementsin efficiency and functionality. These efforts created compilers that form thebackbone of practical secure computation research. Unfortunately, many of theartifacts that are being used to demonstrate new research for secure computationare incomplete, incorrect, or unstable, leading to demonstrably erroneousresults and inefficiencies - extending even to the most recently developedcompiler systems. This is a problem because it hampers research and underminesfeasibility tests when other researchers attempt to use these tools. We addressthese problems and present Frigate, a principled compiler and fast circuitinterpreter for secure computation. To ensure correctness we apply bestpractices for compiler design and development, including the use of standarddata structures, helpful negative results, and structured validation testing. Our systematic validation tests include checks on the internal compiler state, combinations of operators, and edge cases based on widely used techniques anderrors we have observed in other work. This produces a compiler that buildscorrect circuits, is efficient and extensible. Frigate creates circuits withgate counts comparable to previous work, but does so with compile time speedupsas high as 447x compared with the best results from previous work in circuit compilers. By creating avalidated tool, our compiler will allow future secure computationimplementations to be developed quickly and correctly.
33
Protocols for secure computations
Andrew Chi-Chih Yao · 1982 · 2.9K citations
Formal verification of a realistic compiler
Xavier Leroy · Communications of the ACM · 2009 · 1.1K citations · Full text
Fairplay—a secure two-party computation system
Dahlia Malkhi, Noam Nisan, Benny Pinkas et al. · 2004 · 780 citations
Finding and understanding bugs in C compilers
Xuejun Yang, Yang Chen, Eric Eide et al. · 2011 · 714 citations