Visible to the public Biblio

Filters: Keyword is compiler security  [Clear All Filters]
2021-03-15
Kumar, N., Rathee, M., Chandran, N., Gupta, D., Rastogi, A., Sharma, R..  2020.  CrypTFlow: Secure TensorFlow Inference. 2020 IEEE Symposium on Security and Privacy (SP). :336–353.
We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we build three components. Our first component, Athos, is an end-to-end compiler from TensorFlow to a variety of semihonest MPC protocols. The second component, Porthos, is an improved semi-honest 3-party protocol that provides significant speedups for TensorFlow like applications. Finally, to provide malicious secure MPC protocols, our third component, Aramis, is a novel technique that uses hardware with integrity guarantees to convert any semi-honest MPC protocol into an MPC protocol that provides malicious security. The malicious security of the protocols output by Aramis relies on integrity of the hardware and semi-honest security of MPC. Moreover, our system matches the inference accuracy of plaintext TensorFlow.We experimentally demonstrate the power of our system by showing the secure inference of real-world neural networks such as ResNet50 and DenseNet121 over the ImageNet dataset with running times of about 30 seconds for semi-honest security and under two minutes for malicious security. Prior work in the area of secure inference has been limited to semi-honest security of small networks over tiny datasets such as MNIST or CIFAR. Even on MNIST/CIFAR, CrypTFlow outperforms prior work.
Khuchit, U., Wu, L., Zhang, X., Yin, Y., Batsukh, A., Mongolyn, B., Chinbat, M..  2020.  Hardware Design of Polynomial Multiplication for Byte-Level Ring-LWE Based Cryptosystem. 2020 IEEE 14th International Conference on Anti-counterfeiting, Security, and Identification (ASID). :86–89.
An ideal lattice is defined over a ring learning with errors (Ring-LWE) problem. Polynomial multiplication over the ring is the most computational and time-consuming block in lattice-based cryptography. This paper presents the first hardware design of the polynomial multiplication for LAC, one of the Round-2 candidates of the NIST PQC Standardization Process, which has byte-level modulus p=251. The proposed architecture supports polynomial multiplications for different degree n (n=512/1024/2048). For designing the scheme, we used the Vivado HLS compiler, a high-level synthesis based hardware design methodology, which is able to optimize software algorithms into actual hardware products. The design of the scheme takes 274/280/291 FFs and 204/217/208 LUTs on the Xilinx Artix-7 family FPGA, requested by NIST PQC competition for hardware implementation. Multiplication core uses only 1/1/2 pieces of 18Kb BRAMs, 1/1/1 DSPs, and 90/94/95 slices on the board. Our timing result achieved in an alternative degree n with 5.052/4.3985/5.133ns.
Chowdhuryy, M. H. Islam, Liu, H., Yao, F..  2020.  BranchSpec: Information Leakage Attacks Exploiting Speculative Branch Instruction Executions. 2020 IEEE 38th International Conference on Computer Design (ICCD). :529–536.
Recent studies on attacks exploiting processor hardware vulnerabilities have raised significant concern for information security. Particularly, transient execution attacks such as Spectre augment microarchitectural side channels with speculative executions that lead to exfiltration of secretive data not intended to be accessed. Many prior works have demonstrated the manipulation of branch predictors for triggering speculative executions, and thereafter leaking sensitive information through processor microarchitectural components. In this paper, we present a new class of microarchitectural attack, called BranchSpec, that performs information leakage by exploiting state changes of branch predictors in speculative path. Our key observation is that, branch instruction executions in speculative path alter the states of branch pattern history, which are not restored even after the speculatively executed branches are eventually squashed. Unfortunately, this enables adversaries to harness branch predictors as the transmitting medium in transient execution attacks. More importantly, as compared to existing speculative attacks (e.g., Spectre), BranchSpec can take advantage of much simpler code patterns in victim's code base, making the impact of such exploitation potentially even more severe. To demonstrate this security vulnerability, we have implemented two variants of BranchSpec attacks: a side channel where a malicious spy process infers cross-boundary secrets via victim's speculatively executed nested branches, and a covert channel that communicates secrets through intentionally perturbing the branch pattern history structure via speculative branch executions. Our evaluation on Intel Skylake- and Coffee Lake-based processors reveals that these information leakage attacks are highly accurate and successful. To the best of our knowledge, this is the first work to reveal the information leakage threat due to speculative state update in branch predictor. Our studies further broaden the attack surface of processor microarchitecture, and highlight the needs for branch prediction mechanisms that are secure in transient executions.
Simon, L., Verma, A..  2020.  Improving Fuzzing through Controlled Compilation. 2020 IEEE European Symposium on Security and Privacy (EuroS P). :34–52.
We observe that operations performed by standard compilers harm fuzzing because the optimizations and the Intermediate Representation (IR) lead to transformations that improve execution speed at the expense of fuzzing. To remedy this problem, we propose `controlled compilation', a set of techniques to automatically re-factor a program's source code and cherry pick beneficial compiler optimizations to improve fuzzing. We design, implement and evaluate controlled compilation by building a new toolchain with Clang/LLVM. We perform an evaluation on 10 open source projects and compare the results of AFL to state-of-the-art grey-box fuzzers and concolic fuzzers. We show that when programs are compiled with this new toolchain, AFL covers 30 % new code on average and finds 21 additional bugs in real world programs. Our study reveals that controlled compilation often covers more code and finds more bugs than state-of-the-art fuzzing techniques, without the need to write a fuzzer from scratch or resort to advanced techniques. We identify two main reasons to explain why. First, it has proven difficult for researchers to appropriately configure existing fuzzers such as AFL. To address this problem, we provide guidelines and new LLVM passes to help automate AFL's configuration. This will enable researchers to perform a fairer comparison with AFL. Second, we find that current coverage-based evaluation measures (e.g. the total number of visited lines, edges or BBs) are inadequate because they lose valuable information such as which parts of a program a fuzzer actually visits and how consistently it does so. Coverage is considered a useful metric to evaluate a fuzzer's performance and devise a fuzzing strategy. However, the lack of a standard methodology for evaluating coverage remains a problem. To address this, we propose a rigorous evaluation methodology based on `qualitative coverage'. Qualitative coverage uniquely identifies each program line to help understand which lines are commonly visited by different fuzzers vs. which lines are visited only by a particular fuzzer. Throughout our study, we show the benefits of this new evaluation methodology. For example we provide valuable insights into the consistency of fuzzers, i.e. their ability to cover the same code or find the same bug across multiple independent runs. Overall, our evaluation methodology based on qualitative coverage helps to understand if a fuzzer performs better, worse, or is complementary to another fuzzer. This helps security practitioners adjust their fuzzing strategies.
Cortiñas, C. T., Vassena, M., Russo, A..  2020.  Securing Asynchronous Exceptions. 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). :214–229.

Language-based information-flow control (IFC) techniques often rely on special purpose, ad-hoc primitives to address different covert channels that originate in the runtime system, beyond the scope of language constructs. Since these piecemeal solutions may not compose securely, there is a need for a unified mechanism to control covert channels. As a first step towards this goal, we argue for the design of a general interface that allows programs to safely interact with the runtime system and the available computing resources. To coordinate the communication between programs and the runtime system, we propose the use of asynchronous exceptions (interrupts), which, to the best of our knowledge, have not been considered before in the context of IFC languages. Since asynchronous exceptions can be raised at any point during execution-often due to the occurrence of an external event-threads must temporarily mask them out when manipulating locks and shared data structures to avoid deadlocks and, therefore, breaking program invariants. Crucially, the naive combination of asynchronous exceptions with existing features of IFC languages (e.g., concurrency and synchronization variables) may open up new possibilities of information leakage. In this paper, we present MACasync, a concurrent, statically enforced IFC language that, as a novelty, features asynchronous exceptions. We show how asynchronous exceptions easily enable (out of the box) useful programming patterns like speculative execution and some degree of resource management. We prove that programs in MACasync satisfy progress-sensitive non-interference and mechanize our formal claims in the Agda proof assistant.

Danilova, A., Naiakshina, A., Smith, M..  2020.  One Size Does Not Fit All: A Grounded Theory and Online Survey Study of Developer Preferences for Security Warning Types. 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE). :136–148.
A wide range of tools exist to assist developers in creating secure software. Many of these tools, such as static analysis engines or security checkers included in compilers, use warnings to communicate security issues to developers. The effectiveness of these tools relies on developers heeding these warnings, and there are many ways in which these warnings could be displayed. Johnson et al. [46] conducted qualitative research and found that warning presentation and integration are main issues. We built on Johnson et al.'s work and examined what developers want from security warnings, including what form they should take and how they should integrate into their workflow and work context. To this end, we conducted a Grounded Theory study with 14 professional software developers and 12 computer science students as well as a focus group with 7 academic researchers to gather qualitative insights. To back up the theory developed from the qualitative research, we ran a quantitative survey with 50 professional software developers. Our results show that there is significant heterogeneity amongst developers and that no one warning type is preferred over all others. The context in which the warnings are shown is also highly relevant, indicating that it is likely to be beneficial if IDEs and other development tools become more flexible in their warning interactions with developers. Based on our findings, we provide concrete recommendations for both future research as well as how IDEs and other security tools can improve their interaction with developers.
Bresch, C., Lysecky, R., Hély, D..  2020.  BackFlow: Backward Edge Control Flow Enforcement for Low End ARM Microcontrollers. 2020 Design, Automation Test in Europe Conference Exhibition (DATE). :1606–1609.
This paper presents BackFlow, a compiler-based toolchain that enforces indirect backward edge control flow integrity for low-end ARM Cortex-M microprocessors. BackFlow is implemented within the Clang/LLVM compiler and supports the ARM instruction set and its subset Thumb. The control flow integrity generated by the compiler relies on a bitmap, where each set bit indicates a valid pointer destination. The efficiency of the framework is benchmarked using an STM32 NUCLEO F446RE microcontroller. The obtained results show that the control flow integrity solution incurs an execution time overhead ranging from 1.5 to 4.5%.
Piessens, F..  2020.  Security across abstraction layers: old and new examples. 2020 IEEE European Symposium on Security and Privacy Workshops (EuroS PW). :271–279.
A common technique for building ICT systems is to build them as successive layers of bstraction: for instance, the Instruction Set Architecture (ISA) is an abstraction of the hardware, and compilers or interpreters build higher level abstractions on top of the ISA.The functionality of an ICT application can often be understood by considering only a single level of abstraction. For instance the source code of the application defines the functionality using the level of abstraction of the source programming language. Functionality can be well understood by just studying this source code.Many important security issues in ICT system however are cross-layer issues: they can not be understood by considering the system at a single level of abstraction, but they require understanding how multiple levels of abstraction are implemented. Attacks may rely on, or exploit, implementation details of one or more layers below the source code level of abstraction.The purpose of this paper is to illustrate this cross-layer nature of security by discussing old and new examples of cross-layer security issues, and by providing a classification of these issues.
Azahari, A. M., Ahmad, A., Rahayu, S. B., Halip, M. H. Mohamed.  2020.  CheckMyCode: Assignment Submission System with Cloud-Based Java Compiler. 2020 8th International Conference on Information Technology and Multimedia (ICIMU). :343–347.
Learning programming language of Java is a basic part of the Computer Science and Engineering curriculum. Specific Java compiler is a requirement for writing and convert the writing code to executable format. However, some local installed Java compiler is suffering from compatibility, portability and storage space issues. These issues sometimes affect student-learning interest and slow down the learning process. This paper is directed toward the solution for such problems, which offers a new programming assignment submission system with cloud-based Java compiler and is known as CheckMyCode. Leveraging cloud-computing technology in terms of its availability, prevalence and affordability, CheckMyCode implements Java cloud-based programming compiler as a part of the assignment management system. CheckMyCode system is a cloud-based system that allows both main users, which are a lecturer and student to access the system via a browser on PC or smart devices. Modules of submission assignment system with cloud compiler allow lecturer and student to manage Java programming task in one platform. A framework, system module, main user and feature of CheckMyCode are presented. Also, taking into account are the future study/direction and new enhancement of CheckMyCode.
Hwang, S., Ryu, S..  2020.  Gap between Theory and Practice: An Empirical Study of Security Patches in Solidity. 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE). :542–553.
Ethereum, one of the most popular blockchain platforms, provides financial transactions like payments and auctions through smart contracts. Due to the immense interest in smart contracts in academia, the research community of smart contract security has made a significant improvement recently. Researchers have reported various security vulnerabilities in smart contracts, and developed static analysis tools and verification frameworks to detect them. However, it is unclear whether such great efforts from academia has indeed enhanced the security of smart contracts in reality. To understand the security level of smart contracts in the wild, we empirically studied 55,046 real-world Ethereum smart contracts written in Solidity, the most popular programming language used by Ethereum smart contract developers. We first examined how many well-known vulnerabilities the Solidity compiler has patched, and how frequently the Solidity team publishes compiler releases. Unfortunately, we observed that many known vulnerabilities are not yet patched, and some patches are not even sufficient to avoid their target vulnerabilities. Subsequently, we investigated whether smart contract developers use the most recent compiler with vulnerabilities patched. We reported that developers of more than 98% of real-world Solidity contracts still use older compilers without vulnerability patches, and more than 25% of the contracts are potentially vulnerable due to the missing security patches. To understand actual impacts of the missing patches, we manually investigated potentially vulnerable contracts that are detected by our static analyzer and identified common mistakes by Solidity developers, which may cause serious security issues such as financial loss. We detected hundreds of vulnerable contracts and about one fourth of the vulnerable contracts are used by thousands of people. We recommend the Solidity team to make patches that resolve known vulnerabilities correctly, and developers to use the latest Solidity compiler to avoid missing security patches.
Brauckmann, A., Goens, A., Castrillon, J..  2020.  ComPy-Learn: A toolbox for exploring machine learning representations for compilers. 2020 Forum for Specification and Design Languages (FDL). :1–4.
Deep Learning methods have not only shown to improve software performance in compiler heuristics, but also e.g. to improve security in vulnerability prediction or to boost developer productivity in software engineering tools. A key to the success of such methods across these use cases is the expressiveness of the representation used to abstract from the program code. Recent work has shown that different such representations have unique advantages in terms of performance. However, determining the best-performing one for a given task is often not obvious and requires empirical evaluation. Therefore, we present ComPy-Learn, a toolbox for conveniently defining, extracting, and exploring representations of program code. With syntax-level language information from the Clang compiler frontend and low-level information from the LLVM compiler backend, the tool supports the construction of linear and graph representations and enables an efficient search for the best-performing representation and model for tasks on program code.
2020-09-18
Guo, Xiaolong, Dutta, Raj Gautam, He, Jiaji, Tehranipoor, Mark M., Jin, Yier.  2019.  QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment. 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). :91—100.
Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.
2019-12-02
Li, Congwu, Lin, Jingqiang, Cai, Quanwei, Luo, Bo.  2018.  Peapods: OS-Independent Memory Confidentiality for Cryptographic Engines. 2018 IEEE Intl Conf on Parallel Distributed Processing with Applications, Ubiquitous Computing Communications, Big Data Cloud Computing, Social Computing Networking, Sustainable Computing Communications (ISPA/IUCC/BDCloud/SocialCom/SustainCom). :862–869.
Cryptography is widely adopted in computer systems to protect the confidentiality of sensitive information. The security relies on the assumption that cryptography keys are never leaked, which may be broken by the memory disclosure attacks, e.g., the Heartbleed and coldboot attacks. Various schemes are proposed to defend against memory disclosure attacks, e.g., performing the cryptographic computations in registers, or adopting the hardware features (e.g., Intel TSX and Intel SGX) to ensure that the plaintext of the cryptography key never appears in memory. However, these schemes are still not widely deployed due to the following limitations: (a) Most of the schemes are deployed in the OS kernel and require the root (or administrator) privileges of the host; and (b) They require the programmers to integrate these protection schemes in the implementation of different cryptography algorithms on different platforms. In this paper, we propose a tool implemented in Clang/LLVM, named Peapods, which provides the user-mode protection for cryptographic keys in software engines. It introduces one qualifier and three intrinsics for the programmers to specify the sensitive variables and code fragments to be protected, making it easier to be deployed. Peapods adopts transactional memory to protect cryptographic keys, while it is OS-independent and does not require the cryptographic computation performed in the OS kernel. Peapods supports the automatic protection between transactions for better performance. We have implemented the prototype of Peapods. Evaluation results demonstrate that Peapods achieves the design goals with a modest overhead (less than 10%).
Torkura, Kennedy A., Sukmana, Muhammad I.H., Kayem, Anne V.D.M., Cheng, Feng, Meinel, Christoph.  2018.  A Cyber Risk Based Moving Target Defense Mechanism for Microservice Architectures. 2018 IEEE Intl Conf on Parallel Distributed Processing with Applications, Ubiquitous Computing Communications, Big Data Cloud Computing, Social Computing Networking, Sustainable Computing Communications (ISPA/IUCC/BDCloud/SocialCom/SustainCom). :932–939.
Microservice Architectures (MSA) structure applications as a collection of loosely coupled services that implement business capabilities. The key advantages of MSA include inherent support for continuous deployment of large complex applications, agility and enhanced productivity. However, studies indicate that most MSA are homogeneous, and introduce shared vulnerabilites, thus vulnerable to multi-step attacks, which are economics-of-scale incentives to attackers. In this paper, we address the issue of shared vulnerabilities in microservices with a novel solution based on the concept of Moving Target Defenses (MTD). Our mechanism works by performing risk analysis against microservices to detect and prioritize vulnerabilities. Thereafter, security risk-oriented software diversification is employed, guided by a defined diversification index. The diversification is performed at runtime, leveraging both model and template based automatic code generation techniques to automatically transform programming languages and container images of the microservices. Consequently, the microservices attack surfaces are altered thereby introducing uncertainty for attackers while reducing the attackability of the microservices. Our experiments demonstrate the efficiency of our solution, with an average success rate of over 70% attack surface randomization.
Protzenko, Jonathan, Beurdouche, Benjamin, Merigoux, Denis, Bhargavan, Karthikeyan.  2019.  Formally Verified Cryptographic Web Applications in WebAssembly. 2019 IEEE Symposium on Security and Privacy (SP). :1256–1274.
After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these components are often implemented in JavaScript, a language that is both hostile to cryptographic code and hard to reason about. So we instead target WebAssembly, a new instruction set that is supported by all major JavaScript runtimes. We present a new toolchain that compiles Low*, a low-level subset of the F* programming language, into WebAssembly. Unlike other WebAssembly compilers like Emscripten, our compilation pipeline is focused on compactness and auditability: we formalize the full translation rules in the paper and implement it in a few thousand lines of OCaml. Using this toolchain, we present two case studies. First, we build WHACL*, a WebAssembly version of the existing, verified HACL* cryptographic library. Then, we present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.
Abate, Carmine, Blanco, Roberto, Garg, Deepak, Hritcu, Catalin, Patrignani, Marco, Thibault, Jérémy.  2019.  Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :256–25615.
Good programming languages provide helpful abstractions for writing secure code, but the security properties of the source language are generally not preserved when compiling a program and linking it with adversarial code in a low-level target language (e.g., a library or a legacy application). Linked target code that is compromised or malicious may, for instance, read and write the compiled program's data and code, jump to arbitrary memory locations, or smash the stack, blatantly violating any source-level abstraction. By contrast, a fully abstract compilation chain protects source-level abstractions all the way down, ensuring that linked adversarial target code cannot observe more about the compiled program than what some linked source code could about the source program. However, while research in this area has so far focused on preserving observational equivalence, as needed for achieving full abstraction, there is a much larger space of security properties one can choose to preserve against linked adversarial code. And the precise class of security properties one chooses crucially impacts not only the supported security goals and the strength of the attacker model, but also the kind of protections a secure compilation chain has to introduce. 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 abstraction, and some of which provide strictly stronger security guarantees. For each of the studied criteria we propose an equivalent “property-free” characterization that clarifies which proof techniques apply. For relational properties and hyperproperties, which relate the behaviors of multiple programs, our formal definitions of the property classes themselves are novel. We order our criteria by their relative strength and show several collapses and separation results. Finally, we adapt existing proof techniques to show that even the strongest of our secure compilation criteria, the robust preservation of all relational hyperproperties, is achievable for a simple translation from a statically typed to a dynamically typed language.
Burow, Nathan, Zhang, Xinping, Payer, Mathias.  2019.  SoK: Shining Light on Shadow Stacks. 2019 IEEE Symposium on Security and Privacy (SP). :985–999.

Control-Flow Hijacking attacks are the dominant attack vector against C/C++ programs. Control-Flow Integrity (CFI) solutions mitigate these attacks on the forward edge, i.e., indirect calls through function pointers and virtual calls. Protecting the backward edge is left to stack canaries, which are easily bypassed through information leaks. Shadow Stacks are a fully precise mechanism for protecting backwards edges, and should be deployed with CFI mitigations. We present a comprehensive analysis of all possible shadow stack mechanisms along three axes: performance, compatibility, and security. For performance comparisons we use SPEC CPU2006, while security and compatibility are qualitatively analyzed. Based on our study, we renew calls for a shadow stack design that leverages a dedicated register, resulting in low performance overhead, and minimal memory overhead, but sacrifices compatibility. We present case studies of our implementation of such a design, Shadesmar, on Phoronix and Apache to demonstrate the feasibility of dedicating a general purpose register to a security monitor on modern architectures, and Shadesmar's deployability. Our comprehensive analysis, including detailed case studies for our novel design, allows compiler designers and practitioners to select the correct shadow stack design for different usage scenarios. Shadow stacks belong to the class of defense mechanisms that require metadata about the program's state to enforce their defense policies. Protecting this metadata for deployed mitigations requires in-process isolation of a segment of the virtual address space. Prior work on defenses in this class has relied on information hiding to protect metadata. We show that stronger guarantees are possible by repurposing two new Intel x86 extensions for memory protection (MPX), and page table control (MPK). Building on our isolation efforts with MPX and MPK, we present the design requirements for a dedicated hardware mechanism to support intra-process memory isolation, and discuss how such a mechanism can empower the next wave of highly precise software security mitigations that rely on partially isolated information in a process.

Sengupta, Anirban, Kachave, Deepak.  2018.  Integrating Compiler Driven Transformation and Simulated Annealing Based Floorplan for Optimized Transient Fault Tolerant DSP Cores. 2018 IEEE International Symposium on Smart Electronic Systems (iSES) (Formerly iNiS). :17–20.
Reliability of electronic devices in sub-nanometer technology scale has become a major concern. However, demand for battery operated low power, high performance devices necessitates technology scaling. To meet these contradictory design goals optimization and reliability must be performed simultaneously. This paper proposes by integrating compiler driven transformation and simulated annealing based optimization process for generating optimized low cost transient fault tolerant DSP core. The case study on FIR filter shows improved performance (in terms of reduced area and delay) of proposed approach in comparison to state-of-art transient fault tolerant approach.
Kelly, Daniel M., Wellons, Christopher C., Coffman, Joel, Gearhart, Andrew S..  2019.  Automatically Validating the Effectiveness of Software Diversity Schemes. 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks – Supplemental Volume (DSN-S). :1–2.
Software diversity promises to invert the current balance of power in cybersecurity by preventing exploit reuse. Nevertheless, the comparative evaluation of diversity techniques has received scant attention. In ongoing work, we use the DARPA Cyber Grand Challenge (CGC) environment to assess the effectiveness of diversifying compilers in mitigating exploits. Our approach provides a quantitative comparison of diversity strategies and demonstrates wide variation in their effectiveness.
Besson, Frédéric, Dang, Alexandre, Jensen, Thomas.  2019.  Information-Flow Preservation in Compiler Optimisations. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :230–23012.

Correct compilers perform program transformations preserving input/output behaviours of programs. Yet, correctness does not prevent program optimisations from introducing information-flow leaks that would make the target program more vulnerable to side-channel attacks than the source program. To tackle this problem, we propose a notion of Information-Flow Preserving (IFP) program transformation which ensures that a target program is no more vulnerable to passive side-channel attacks than a source program. To protect against a wide range of attacks, we model an attacker who is granted arbitrary memory accesses for a pre-defined set of observation points. We propose a compositional proof principle for proving that a transformation is IFP. Using this principle, we show how a translation validation technique can be used to automatically verify and even close information-flow leaks introduced by standard compiler passes such as dead-store elimination and register allocation. The technique has been experimentally validated on the CompCert C compiler.

Yang, Shouguo, Shi, Zhiqiang, Zhang, Guodong, Li, Mingxuan, Ma, Yuan, Sun, Limin.  2019.  Understand Code Style: Efficient CNN-Based Compiler Optimization Recognition System. ICC 2019 - 2019 IEEE International Conference on Communications (ICC). :1–6.
Compiler optimization level recognition can be applied to vulnerability discovery and binary analysis. Due to the exists of many different compilation optimization options, the difference in the contents of the binary file is very complicated. There are thousands of compiler optimization algorithms and multiple different processor architectures, so it is very difficult to manually analyze binary files and recognize its compiler optimization level with rules. This paper first proposes a CNN-based compiler optimization level recognition model: BinEye. The system extracts semantic and structural differences and automatically recognize the compiler optimization levels. The model is designed to be very suitable for binary file processing and is easy to understand. We built a dataset containing 80028 binary files for the model training and testing. Our proposed model achieves an accuracy of over 97%. At the same time, BinEye is a fully CNN-based system and it has a faster forward calculation speed, at least 8 times faster than the normal RNN-based model. Through our analysis of the model output, we successfully found the difference in assembly codes caused by the different compiler optimization level. This means that the model we proposed is interpretable. Based on our model, we propose a method to analyze the code differences caused by different compiler optimization levels, which has great guiding significance for analyzing closed source compilers and binary security analysis.
Simon, Laurent, Chisnall, David, Anderson, Ross.  2018.  What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. 2018 IEEE European Symposium on Security and Privacy (EuroS P). :1–15.
Security engineers have been fighting with C compilers for years. A careful programmer would test for null pointer dereferencing or division by zero; but the compiler would fail to understand, and optimize the test away. Modern compilers now have dedicated options to mitigate this. But when a programmer tries to control side effects of code, such as to make a cryptographic algorithm execute in constant time, the problem remains. Programmers devise complex tricks to obscure their intentions, but compiler writers find ever smarter ways to optimize code. A compiler upgrade can suddenly and without warning open a timing channel in previously secure code. This arms race is pointless and has to stop. We argue that we must stop fighting the compiler, and instead make it our ally. As a starting point, we analyze the ways in which compiler optimization breaks implicit properties of crypto code; and add guarantees for two of these properties in Clang/LLVM. Our work explores what is actually involved in controlling side effects on modern CPUs with a standard toolchain. Similar techniques can and should be applied to other security properties; achieving intentions by compiler commands or annotations makes them explicit, so we can reason about them. It is already understood that explicitness is essential for cryptographic protocol security and for compiler performance; it is essential for language security too. We therefore argue that this should be only the first step in a sustained engineering effort.
2019-10-14
Koo, H., Chen, Y., Lu, L., Kemerlis, V. P., Polychronakis, M..  2018.  Compiler-Assisted Code Randomization. 2018 IEEE Symposium on Security and Privacy (SP). :461–477.

Despite decades of research on software diversification, only address space layout randomization has seen widespread adoption. Code randomization, an effective defense against return-oriented programming exploits, has remained an academic exercise mainly due to i) the lack of a transparent and streamlined deployment model that does not disrupt existing software distribution norms, and ii) the inherent incompatibility of program variants with error reporting, whitelisting, patching, and other operations that rely on code uniformity. In this work we present compiler-assisted code randomization (CCR), a hybrid approach that relies on compiler-rewriter cooperation to enable fast and robust fine-grained code randomization on end-user systems, while maintaining compatibility with existing software distribution models. The main concept behind CCR is to augment binaries with a minimal set of transformation-assisting metadata, which i) facilitate rapid fine-grained code transformation at installation or load time, and ii) form the basis for reversing any applied code transformation when needed, to maintain compatibility with existing mechanisms that rely on referencing the original code. We have implemented a prototype of this approach by extending the LLVM compiler toolchain, and developing a simple binary rewriter that leverages the embedded metadata to generate randomized variants using basic block reordering. The results of our experimental evaluation demonstrate the feasibility and practicality of CCR, as on average it incurs a modest file size increase of 11.46% and a negligible runtime overhead of 0.28%, while it is compatible with link-time optimization and control flow integrity.

2018-01-10
Patrignani, M., Garg, D..  2017.  Secure Compilation and Hyperproperty Preservation. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :392–404.

The area of secure compilation aims to design compilers which produce hardened code that can withstand attacks from low-level co-linked components. So far, there is no formal correctness criterion for secure compilers that comes with a clear understanding of what security properties the criterion actually provides. Ideally, we would like a criterion that, if fulfilled by a compiler, guarantees that large classes of security properties of source language programs continue to hold in the compiled program, even as the compiled program is run against adversaries with low-level attack capabilities. This paper provides such a novel correctness criterion for secure compilers, called trace-preserving compilation (TPC). We show that TPC preserves a large class of security properties, namely all safety hyperproperties. Further, we show that TPC preserves more properties than full abstraction, the de-facto criterion used for secure compilation. Then, we show that several fully abstract compilers described in literature satisfy an additional, common property, which implies that they also satisfy TPC. As an illustration, we prove that a fully abstract compiler from a typed source language to an untyped target language satisfies TPC.

Garcia, R., Modesti, P..  2017.  An IDE for the Design, Verification and Implementation of Security Protocols. 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). :157–163.

Security protocols are critical components for the construction of secure and dependable distributed applications, but their implementation is challenging and error prone. Therefore, tools for formal modelling and analysis of security protocols can be potentially very useful to support software engineers. However, despite such tools have been available for a long time, their adoption outside the research community has been very limited. In fact, most practitioners find such applications too complex and hardly usable for their daily work. In this paper, we present an Integrated Development Environment for the design, verification and implementation of security protocols, aimed at lowering the adoption barrier of formal methods tools for security. In the spirit of Model Driven Development, the environment supports the user in the specification of the model using the simple and intuitive language AnB (and its extension AnBx). Moreover, it provides a push-button solution for the formal verification of the abstract and concrete models, and for the automatic generation of Java implementation. This Eclipse-based IDE leverages on existing languages and tools for modelling and verification of security protocols, such as the AnBx Compiler and Code Generator, the model checker OFMC and the protocol verifier ProVerif.