More Like this

1. Eliminating timing side-channel leaks using program repair

   https://doi.org/10.1145/3213846.3213851  

   Wu, Meng; Guo, Shengjian; Schaumont, Patrick; Wang, Chao (January 2018, ACM SIGSOFT International Symposium on Software Testing and Analysis)

   We propose a method, based on program analysis and transformation, for eliminating timing side channels in software code that implements security-critical applications. Our method takes as input the original program together with a list of secret variables (e.g., cryptographic keys, security tokens, or passwords) and returns the transformed program as output. The transformed program is guaranteed to be functionally equivalent to the original program and free of both instruction- and cache-timing side channels. Specifically, we ensure that the number of CPU cycles taken to execute any path is independent of the secret data, and the cache behavior of memory accesses, in terms of hits and misses, is independent of the secret data. We have implemented our method in LLVM and validated its effectiveness on a large set of applications, which are cryptographic libraries with 19,708 lines of C/C++ code in total. Our experiments show the method is both scalable for real applications and effective in eliminating timing side channels. 

   more » « less
2. Verifying Fortran Programs with CIVL

   https://doi.org/10.1007/978-3-030-99524-9_6  

   Wu, Wenhao; Hückelheim, Jan; Hovland, Paul D.; Siegel, Stephen F. (March 2022, TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems)

   Fisman, Dana; Rosu, Grigore (Ed.)

   Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran's unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application. 

   more » « less
3. Scaling symbolic evaluation for automated verification of systems code with Serval

   https://doi.org/10.1145/3341301.3359641  

   Nelson, Luke; Bornholt, James; Gu, Ronghui; Baumann, Andrew; Torlak, Emina; Wang, Xi (January 2019, Symposium on Operating Systems Principles)

   This paper presents Serval, a framework for developing au- tomated verifiers for systems software. Serval provides an extensible infrastructure for creating verifiers by lifting interpreters under symbolic evaluation, and a systematic approach to identifying and repairing verification performance bottlenecks using symbolic profiling and optimizations. Using Serval, we build automated verifiers for the RISC-V, x86-32, LLVM, and BPF instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems previously verified using Coq and Dafny, respectively, for automated verification using Serval, and discuss trade-offs of different verification methodologies. In addition, we apply Serval to the Keystone security monitor and the BPF compil- ers in the Linux kernel, and uncover 18 new bugs through verification, all confirmed and fixed by developers. 

   more » « less
4. NOELLE Offers Empowering LLVM Extensions

   https://doi.org/10.1109/CGO53902.2022.9741276  

   Matni, Angelo; Deiana, Enrico Armenio; Su, Yian; Gross, Lukas; Ghosh, Souradip; Apostolakis, Sotiris; Xu, Ziyang; Tan, Zujun; Chaturvedi, Ishita; Homerding, Brian; et al (April 2022, 2022 IEEE/ACM International Symposium on Code Generation and Optimization (CGO))

   Modern and emerging architectures demand increasingly complex compiler analyses and transformations. As the emphasis on compiler infrastructure moves beyond support for peephole optimizations and the extraction of instruction-level parallelism, compilers should support custom tools designed to meet these demands with higher-level analysis-powered abstractions and functionalities of wider program scope. This paper introduces NOELLE, a robust open-source domain-independent compilation layer built upon LLVM providing this support. NOELLE extends abstractions and functionalities provided by LLVM enabling advanced, program-wide code analyses and transformations. This paper shows the power of NOELLE by presenting a diverse set of 11 custom tools built upon it. 

   more » « less
5. CLN2INV: LEARNING LOOP INVARIANTS WITH CONTINUOUS LOGIC NETWORK

   Ryan, Gabriel; Wong, Justin; Yao, Jianan; Gu, Ronghui; Jana, Suman (May 2020, International Conference on Learning Representations)

   Program verification offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind automated verification of real-world programs which often contain many loops. In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces. We develop a new sound and complete semantic mapping for assigning SMT formulas to continuous truth values that allows CLNs to be trained efficiently. We use CLNs to implement a new inference system for loop invariants, CLN2INV, that significantly outperforms existing approaches on the popular Code2Inv dataset. CLN2INV is the first tool to solve all 124 theoretically solvable problems in the Code2Inv dataset. Moreover, CLN2INV takes only 1.1 seconds on average for each problem, which is 40× faster than existing approaches. We further demonstrate that CLN2INV can even learn 12 significantly more complex loop invariants than the ones required for the Code2Inv dataset. 

   more » « less