Secure Synthesis of Distributed Cryptographic Applications (Technical Report)

• URL: http://arxiv.org/abs/2401.04131v1
• Date: Sat, 6 Jan 2024 02:57:44 GMT
• Title: Secure Synthesis of Distributed Cryptographic Applications (Technical Report)
• Authors: Coşku Acay, Joshua Gancher, Rolph Recto, Andrew C. Myers,
• Abstract summary: We advocate using secure program partitioning to synthesize cryptographic applications. This approach is promising, but formal results for the security of such compilers are limited in scope. We develop a compiler security proof that handles subtleties essential for robust, efficient applications.
• Score: 1.9707603524984119
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Multi-Layered Security System: Integrating Quantum Key Distribution with Classical Cryptography to Enhance Steganographic Security [0.0]
  We present a novel cryptographic system that integrates Quantum Key Distribution (QKD) with classical encryption techniques. Our approach leverages the E91 QKD protocol to generate a shared secret key between communicating parties. This key is then hashed using the Secure Hash Algorithm (SHA) to provide a fixedlength, high-entropy key.
  arXiv  Detail & Related papers  (2024-08-13T15:20:29Z)
• Providing High-Performance Execution with a Sequential Contract for Cryptographic Programs [3.34371579019566]
  Constant-time programming is a widely deployed approach to harden cryptographic programs against side channel attacks. Modern processors violate the underlying assumptions of constant-time policies by speculatively executing unintended paths of the program. We propose Cassandra, a novel hardware-software mechanism to protect constant-time cryptographic code against speculative control flow based attacks.
  arXiv  Detail & Related papers  (2024-06-06T17:34:48Z)
• CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
  We propose CodeChameleon, a novel jailbreak framework based on personalized encryption tactics. We conduct extensive experiments on 7 Large Language Models, achieving state-of-the-art average Attack Success Rate (ASR) Remarkably, our method achieves an 86.6% ASR on GPT-4-1106.
  arXiv  Detail & Related papers  (2024-02-26T16:35:59Z)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  We introduce for non-uniform messages a novel hybrid universal network coding cryptosystem (NU-HUNCC) We show that NU-HUNCC is information-theoretic individually secured against an eavesdropper with access to any subset of the links.
  arXiv  Detail & Related papers  (2024-02-13T12:12:39Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• Code Polymorphism Meets Code Encryption: Confidentiality and Side-Channel Protection of Software Components [0.0]
  PolEn is a toolchain and a processor architecturethat combine countermeasures in order to provide an effective mitigation of side-channel attacks. Code encryption is supported by a processor extension such that machineinstructions are only decrypted inside the CPU. Code polymorphism is implemented by software means. It regularly changes the observablebehaviour of the program, making it unpredictable for an attacker.
  arXiv  Detail & Related papers  (2023-10-11T09:16:10Z)
• SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
  We propose SOCI+ which significantly improves the performance of SOCI. SOCI+ employs a novel (2, 2)-threshold Paillier cryptosystem with fast encryption and decryption as its cryptographic primitive. Compared with SOCI, our experimental evaluation shows that SOCI+ is up to 5.4 times more efficient in computation and 40% less in communication overhead.
  arXiv  Detail & Related papers  (2023-09-27T05:19:32Z)
• SemProtector: A Unified Framework for Semantic Protection in Deep Learning-based Semantic Communication Systems [51.97204522852634]
  We present a unified framework that aims to secure an online semantic communications system with three semantic protection modules. Specifically, these protection modules are able to encrypt semantics to be transmitted by an encryption method, mitigate privacy risks from wireless channels by a perturbation mechanism, and calibrate distorted semantics at the destination. Our framework enables an existing online SC system to dynamically assemble the above three pluggable modules to meet customized semantic protection requirements.
  arXiv  Detail & Related papers  (2023-09-04T06:34:43Z)
• Citadel: Real-World Hardware-Software Contracts for Secure Enclaves Through Microarchitectural Isolation and Controlled Speculation [8.414722884952525]
  Hardware isolation primitives such as secure enclaves aim to protect programs, but remain vulnerable to transient execution attacks. This paper advocates for processors to incorporate microarchitectural isolation primitives and mechanisms for controlled speculation. We introduce two mechanisms to securely share memory between an enclave and an untrusted OS in an out-of-order processor.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)
• Securing Optimized Code Against Power Side Channels [1.589424114251205]
  Security engineers often sacrifice code efficiency by turning off compiler optimization and/or performing local, post-compilation transformations. This paper proposes SecConCG, a constraint-based compiler approach that generates optimized yet secure code.
  arXiv  Detail & Related papers  (2022-07-06T12:06:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.