首页/论文/2004.03557

arXiv 2004.035572020-04-07cs.PLcs.LO

A categorical approach to secure compilation

Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

备注：: Accepted in Coalgebraic Methods in Computer Science, ver. 2020

英文摘要：

We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security instead of full abstraction, which is the preservation and reflection of contextual equivalence. To that end, we also make use of the well-behavedness properties of distributive laws to construct a categorical argument for the contextual connotations of bisimilarity.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Robustly Safe Compilation or, Efficient, Provably Secure Compilation

Secure compilers generate compiled code that withstands many target-level attacks such as alteration of control flow, data leaks or memory corruption. Many existing secure compilers are proven to be fully abstract, meaning that they reflect and preserve observational equivalence. Fully abstract compilation is a strong and useful property that, in certain cases, comes at the cost of requiring expensive runtime constructs in compiled code. These constructs may have no relevance for security, but are needed to accommodate differences between the source language and the target language that fully …

2020-11-27cs.PL

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)

We map the space of soundness criteria for secure compilation based on the preservation of hyperproperties in arbitrary adversarial contexts, which we call robust hyperproperty preservation. For this, we study the preservation of several classes of hyperproperties and for each class we propose an equivalent "property-free" characterization of secure compilation that is generally better tailored for proofs. Even the strongest of our soundness criteria, the robust preservation of all hyperproperties, seems achievable for simple transformations and provable using context back-translation techniqu…

2017-12-20cs.CRcs.PL

Contract-Aware Secure Compilation

Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the confidentiality and integrity of a system. To secure systems against microarchitectural attacks, programmers need to reason about and program against these microarchitectural side-effects. However, we cannot -- and should not -- expect programmers to manually tailor programs for specific processors and their security guarantees. Instead, we could rely on compilers (and the secure compilation community), as they can play…

2020-12-28cs.CRcs.PL

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components

Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker model for secure compilation that extends the well-known notion of full abstraction to ensure protection for mutually distrustful components. We devise a compiler chain (compiler, linker, and loader) and a novel security monitor that together defend against this strong attacker model. The monitor is implemented using a recently proposed, generic tag-based protection framework called micro-policies, which comes with hardw…

2015-10-02cs.CRcs.PL

Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)

We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion goes beyond recent proposals, which protect the trace properties of a single component against an adversarial context, to model dynamic compromise in a system of mutually distrustful components. Each component is protected from all the others until it receives an input that triggers an undefined behavior, causing it to become compromised and attack the remaining uncompromised components. To illustrate…

2017-10-31cs.CRcs.PL

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others---in particular, from components that have encountered undefined behavior and become compromised. Each comp…

2019-11-29cs.CRcs.PL

更多相关论文收起更多论文

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation

(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.) We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust property preservation, i.e., the preservation of properties satisfied against arbitrary adversarial contexts. We study robustly preserving various classes of trace properties such as safety, of hyperproperties such as noninterference, and of relational hyperproperties such as trace equivalence. This leads to many new secure compilation criteria, some of which are easier to practically achieve and prove than full abstr…

2019-05-17cs.CRcs.PL

Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation, defined as the preservation of robust satisfaction of hyperproperties, i.e., their satisfaction against arbitrary attackers. In this paper, we initially set out to compare these two approaches to secure compilation. To that end, we provide an exact description of the hyperproperties that are robustly satisfied by programs compiled with a fully abstract compiler, and show that they can be meaningless or trivial. We …

2021-09-20cs.CRcs.PL

SECOMP：分区C程序的形式化安全编译

SECOMP: Formally Secure Compilation of Compartmentalized C Programs

本文提出SECOMP编译器，首次为主流语言C证明类似完全抽象的安全编译准则，将未定义行为限制在遭攻陷的分区内，并通过扩展CompCert及证明工程创新实现形式化安全编译。

2025-01-01cs.CRcs.PL

SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation

Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-translation, one can syntactically translate the target attacker to a source one -- i.e., syntax-directed back-translation -- or show that the interaction traces of the target attacker can also be emitted by source attackers -- i.e., trace-directed back-translation. Syntax-directed back-translation is not suitable when the target attacker may use unstructured control flow that the source language cannot directly represe…

2022-06-03cs.CRcs.PL

On Modular and Fully-Abstract Compilation -- Technical Appendix

Secure compilation studies compilers that generate target-level components that are as secure as their source-level counterparts. Full abstraction is the most widely-proven property when defining a secure compiler. A compiler is modular if it allows different components to be compiled independently and then to be linked together to form a whole program. Unfortunately, many existing fully-abstract compilers to untyped machine code are not modular. So, while fully-abstractly compiled components are secure from malicious attackers, if they are linked against each other the resulting component may…

2016-04-18cs.PL

Translation Validation for Security Properties

Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles.

2019-01-15cs.CRcs.PL

混合敏感并发程序的验证安全编译

Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs

该研究使用Isabelle/HOL验证了一个单遍编译器能够保持混合敏感并发程序的非干扰性，通过引入分解原则简化安全精化证明，并在真实用例上自动保留安全属性。

2022-02-28cs.CRcs.LOcs.PL

用于机械化安全编译证明的调用-返回树的 Nanopass 回译

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

针对安全编译链证明中回译步骤复杂的挑战，提出一种基于调用-返回树、分多步进行的 nanopass 回译技术，利用幽灵状态和前向模拟简化证明，并在 Rocq 证明器中实现了机械化验证。

2025-07-16cs.CRcs.PL

Universal Composability is Robust Compilation

This paper discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC). In cryptography, UC is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied …

2022-12-15cs.CRcs.PL

Secure Optimization Through Opaque Observations

Secure applications implement software protections against side-channel and physical attacks. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. To prevent optimizing compilers from altering the protection, security engineers embed input/output side-effects into the protection. These side-effects are error-prone and compiler-dependent, and the current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. Vu et al. recently demonstrate…

2021-01-15cs.CRcs.PL

Trace-Relating Compiler Correctness and Secure Compilation

Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definitio…

2020-02-23cs.CRcs.PL

计算有界的鲁棒编译与通用可组合安全

Computationally Bounded Robust Compilation and Universally Composable Security

本研究将通用可组合性（UC）与鲁棒编译（RC）的关联拓展至计算场景，构建可推广的通用框架，借助计算不可区分性证明工具实现计算UC安全证明的机械化，并通过CryptoVerif验证Wireguard协议部分安全性，框架证明在Isabelle/HOL中完成验证。

2024-01-26cs.CRcs.PL

保护 F* 中经静态验证的 IO 程序免受未验证代码攻击

Securing Verified IO Programs Against Unverified Code in F*

SCIO* 是一个形式化安全编译框架，通过高阶契约和引用监控，确保 F* 验证的 IO 程序与未验证上下文链接时的安全，并证明其满足强安全编译标准。

2023-11-15cs.PL