Зміст
Добірка наукової літератури з теми "Secure Compilation"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Secure Compilation".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Статті в журналах з теми "Secure Compilation"
1
Vu, Son Tuan, Albert Cohen, Arnaud De Grandmaison, Christophe Guillon, and Karine Heydemann. "Reconciling optimization with secure compilation." Proceedings of the ACM on Programming Languages 5, OOPSLA (2021): 1–30. http://dx.doi.org/10.1145/3485519.
Повний текст джерелаАнотація:
Software protections against side-channel and physical attacks are essential to the development of secure applications. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. This renders them susceptible to miscompilation, and security engineers embed input/output side-effects to prevent optimizing compilers from altering them. Yet these side-effects are error-prone and compiler-dependent. The current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. These side-effects may also be too expensive in fine-grained protections such as control-flow integrity. We introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the input/output semantics-preservation contract of compilers. We introduce an opacification mechanism to preserve and enforce a partial ordering of observations. This approach is compatible with a production compiler and does not incur any modification to its optimization passes. We validate the effectiveness and performance of our approach on a range of benchmarks, expressing the secure compilation of these applications in terms of observations to be made at specific program points.
2
Patrignani, Marco, Amal Ahmed, and Dave Clarke. "Formal Approaches to Secure Compilation." ACM Computing Surveys 51, no. 6 (2019): 1–36. http://dx.doi.org/10.1145/3280984.
Повний текст джерела
3
Patrignani, Marco, and Deepak Garg. "Robustly Safe Compilation, an Efficient Form of Secure Compilation." ACM Transactions on Programming Languages and Systems 43, no. 1 (2021): 1–41. http://dx.doi.org/10.1145/3436809.
Повний текст джерелаАнотація:
Security-preserving compilers generate compiled code that withstands target-level attacks such as alteration of control flow, data leaks, or memory corruption. Many existing security-preserving compilers are proven to be fully abstract, meaning that they reflect and preserve observational equivalence. Fully abstract compilation is strong and useful but, 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 and target languages that fully abstract compilation necessarily needs. As an alternative to fully abstract compilation, this article explores a different criterion for secure compilation called robustly safe compilation or RSC . Briefly, this criterion means that the compiled code preserves relevant safety properties of the source program against all adversarial contexts interacting with the compiled program. We show that RSC can be proved more easily than fully abstract compilation and also often results in more efficient code. We also present two different proof techniques for establishing that a compiler attains RSC and, to illustrate them, develop three illustrative robustly safe compilers that rely on different target-level protection mechanisms. We then proceed to turn one of our compilers into a fully abstract one and through this example argue that proving RSC can be simpler than proving full abstraction. To better explain and clarify notions, this article uses syntax highlighting in a way that colourblind and black-8-white readers can benefit from Reference [58]. For a better experience, please print or view this article in colour . 1
4
Patrignani, Marco, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. "Secure Compilation to Protected Module Architectures." ACM Transactions on Programming Languages and Systems 37, no. 2 (2015): 1–50. http://dx.doi.org/10.1145/2699503.
Повний текст джерела
5
Abate, Carmine, Roberto Blanco, Ştefan Ciobâcă, et al. "An Extended Account of Trace-relating Compiler Correctness and Secure Compilation." ACM Transactions on Programming Languages and Systems 43, no. 4 (2021): 1–48. http://dx.doi.org/10.1145/3460860.
Повний текст джерелаАнотація:
Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be 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 definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.
6
Andrici, Cezar-Constantin, Ștefan Ciobâcă, Cătălin Hriţcu, et al. "Securing Verified IO Programs Against Unverified Code in F*." Proceedings of the ACM on Programming Languages 8, POPL (2024): 2226–59. http://dx.doi.org/10.1145/3632916.
Повний текст джерелаАнотація:
We introduce SCIO*, a formally secure compilation framework for statically verified programs performing input-output (IO). The source language is an F* subset in which a verified program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F* subset in which the compiled program is linked with an adversarial context that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the state of the monitor. But these checks cannot stop the adversarial target context before it performs dangerous IO operations. Therefore linking in SCIO* additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F* that SCIO* soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F* that SCIO* satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO* at work on a simple web server example.
7
Blanton, Marina, Dennis Murphy, and Chen Yuan. "Efficiently Compiling Secure Computation Protocols From Passive to Active Security: Beyond Arithmetic Circuits." Proceedings on Privacy Enhancing Technologies 2024, no. 1 (2024): 74–97. http://dx.doi.org/10.56553/popets-2024-0006.
Повний текст джерелаАнотація:
This work studies compilation of honest-majority semi-honest secure multi-party protocols secure up to additive attacks to maliciously secure computation with abort. Prior work concentrated on arithmetic circuits composed of addition and multiplication gates, while many practical protocols rely on additional types of elementary operations or gates to achieve good performance. In this work we revisit the notion of security up to additive attacks in the presence of additional gates such as random element generation and opening. This requires re-evaluation of functions that can be securely evaluated, extending the notion of protocols secure up to additive attacks, and re-visiting the notion of delayed verification that points to weaknesses in its prior use and designing a mitigation strategy. We transform the computation using dual execution to achieve security in the malicious model with abort and experimentally evaluate the difference in performance of semi-honest and malicious protocols to demonstrate the low cost.
8
G, Selvakumar. "A Novel Approach for Remote Compilation using Docker Containers." International Journal of Computer Communication and Informatics 1, no. 1 (2019): 46–51. http://dx.doi.org/10.34256/ijcci1918.
Повний текст джерелаАнотація:
The number of programming languages is getting more and more and developers are facing a tough time in installing all the compilers, libraries and supporting files for the development activities. Most of the time they want to experiment with new technologies, where the efforts required creating a complete environment to run the programs may not be feasible. On the other hand, several companies have started recruiting developers through their online programming platforms. In such situations, it is essential to protect the resources of the server from malicious programs written by the users by purpose or inadvertently. The client environment has to be as lighter as possible and the server environment must be as secure and efficient as possible. There are several existing solutions to meet this objective with plenty of demerits. In this paper we propose a novel method which overcomes most of the problems in the existing solutions and we have experimented the effectiveness of the proposed solution. In our proposed method we develop a docker based sandbox to run the client programs and display the output. We have developed a complete web interface to test the solution and created a backend to manage the users, sessions, tested programs and the outcomes which can be used for analytics too.
9
Jawade, Prashant Balkrishna, and S. Ramachandram. "Multi-objective secure task scheduling based on SLA in multi-cloud environment." Multiagent and Grid Systems 18, no. 1 (2022): 65–85. http://dx.doi.org/10.3233/mgs-220362.
Повний текст джерелаАнотація:
The appliances that are received at a cloud data centre are a compilation of jobs (task) that might be independent or dependent on one another. These tasks are then allocated to diverse virtual machine (VM) in a scheduled way. For this task allocation, various scheduling policies are deployed with the intention of reducing energy utilization and makespan, and increasing cloud resource exploitation as well. A variety of research and studies were done to attain an optimal solution in a single cloud setting, however the similar schemes might not operate on multi-cloud environments. Here, this paper aims to introduce a secured task scheduling model in multi-cloud environment. The developed approach mainly concerns on optimal allocation of tasks via a hybrid optimization theory. Consequently, the developed optimal task allotment considers the objectives like makespan, execution time, security parameters (risk evaluation), utilization cost, maximal service level agreement (SLA) adherence and power usage effectiveness (PUE). For resolving this issue, a novel hybrid algorithm termed as rock hyraxes updated shark smell with logistic mapping (RHU-SLM) is introduced in this work. At last, the superiority of developed approach is proved on varied measures.
10
Zhang, Denghui, Lijing Ren, and Zhaoquan Gu. "Enhancing the Privacy of Network Services through Trusted Computing." Applied Sciences 12, no. 18 (2022): 9191. http://dx.doi.org/10.3390/app12189191.
Повний текст джерелаАнотація:
The addressing and discovering service is a vital infrastructure of the Internet. New applications and scenarios in next-generation networks rely on the secure and stable operation of domain name services, which puts forward new security challenges for the original domain name mechanism. While previous security enhancements of network services struggled to strike a balance between security, performance, and compatibility, hindering further use of core network services, the TEE (Trusted Computing Environment) technology can provide trusted and confidential services in untrusted network environments by verifiable hardware signatures. In this paper, we present a novel trustworthy service architecture with the preservation of security and privacy for addressing messages. The scheme provides a secure enclave to generate authenticatable responses between clients and targets, thus ensuring the privacy of services. We further build a new TEE compilation model to ensure that the built resolver application can provide trusted and secure services within TEE while keeping the availability without the TEE hardware. Experimental results show that our approach can enhance the privacy and security of addressing services such as DNS (Domain Name System) without sacrificing the quality of service and breaking the infrastructures of existing services.