Visible to the public Biblio

Filters: Keyword is program diagnostics  [Clear All Filters]
2020-07-10
Nahmias, Daniel, Cohen, Aviad, Nissim, Nir, Elovici, Yuval.  2019.  TrustSign: Trusted Malware Signature Generation in Private Clouds Using Deep Feature Transfer Learning. 2019 International Joint Conference on Neural Networks (IJCNN). :1—8.

This paper presents TrustSign, a novel, trusted automatic malware signature generation method based on high-level deep features transferred from a VGG-19 neural network model pre-trained on the ImageNet dataset. While traditional automatic malware signature generation techniques rely on static or dynamic analysis of the malware's executable, our method overcomes the limitations associated with these techniques by producing signatures based on the presence of the malicious process in the volatile memory. Signatures generated using TrustSign well represent the real malware behavior during runtime. By leveraging the cloud's virtualization technology, TrustSign analyzes the malicious process in a trusted manner, since the malware is unaware and cannot interfere with the inspection procedure. Additionally, by removing the dependency on the malware's executable, our method is capable of signing fileless malware. Thus, we focus our research on in-browser cryptojacking attacks, which current antivirus solutions have difficulty to detect. However, TrustSign is not limited to cryptojacking attacks, as our evaluation included various ransomware samples. TrustSign's signature generation process does not require feature engineering or any additional model training, and it is done in a completely unsupervised manner, obviating the need for a human expert. Therefore, our method has the advantage of dramatically reducing signature generation and distribution time. The results of our experimental evaluation demonstrate TrustSign's ability to generate signatures invariant to the process state over time. By using the signatures generated by TrustSign as input for various supervised classifiers, we achieved 99.5% classification accuracy.

2020-07-09
Ashouri, Mohammadreza.  2019.  Detecting Input Sanitization Errors in Scala. 2019 Seventh International Symposium on Computing and Networking Workshops (CANDARW). :313—319.

Scala programming language combines object-oriented and functional programming in one concise, high-level language, and the language supports static types that help to avoid bugs in complex programs. This paper proposes a dynamic taint analyzer called ScalaTaint for Scala applications. The analyzer traces the propagation of malicious inputs from untrusted sources to sensitive sink methods in programs that can be exploited by adversaries. In this work, we evaluated the accuracy of ScalaTaint with a security benchmark suite including 7 projects in Scala. As a result, our analyzer could report 49 vulnerabilities within 753,372 lines of code. Moreover, the result of our performance measurement on ScalaBench shows 67% runtime overhead that demonstrates the usefulness and efficiently of our technique in comparison with similar tools.

2020-06-26
Puccetti, Armand.  2019.  The European H2020 project VESSEDIA (Verification Engineering of Safety and SEcurity critical Dynamic Industrial Applications). 2019 22nd Euromicro Conference on Digital System Design (DSD). :588—591.

This paper presents an overview of the H2020 project VESSEDIA [9] aimed at verifying the security and safety of modern connected systems also called IoT. The originality relies in using Formal Methods inherited from high-criticality applications domains to analyze the source code at different levels of intensity, to gather possible faults and weaknesses. The analysis methods are mostly exhaustive an guarantee that, after analysis, the source code of the application is error-free. This paper is structured as follows: after an introductory section 1 giving some factual data, section 2 presents the aims and the problems addressed; section 3 describes the project's use-cases and section 4 describes the proposed approach for solving these problems and the results achieved until now; finally, section 5 discusses some remaining future work.

2020-04-24
Ogale, Pushkar, Shin, Michael, Abeysinghe, Sasanka.  2018.  Identifying Security Spots for Data Integrity. 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC). 02:462—467.

This paper describes an approach to detecting malicious code introduced by insiders, which can compromise the data integrity in a program. The approach identifies security spots in a program, which are either malicious code or benign code. Malicious code is detected by reviewing each security spot to determine whether it is malicious or benign. The integrity breach conditions (IBCs) for object-oriented programs are specified to identify security spots in the programs. The IBCs are specified by means of the concepts of coupling within an object or between objects. A prototype tool is developed to validate the approach with a case study.

2020-04-20
Huang, Zhen, Lie, David, Tan, Gang, Jaeger, Trent.  2019.  Using Safety Properties to Generate Vulnerability Patches. 2019 IEEE Symposium on Security and Privacy (SP). :539–554.
Security vulnerabilities are among the most critical software defects in existence. When identified, programmers aim to produce patches that prevent the vulnerability as quickly as possible, motivating the need for automatic program repair (APR) methods to generate patches automatically. Unfortunately, most current APR methods fall short because they approximate the properties necessary to prevent the vulnerability using examples. Approximations result in patches that either do not fix the vulnerability comprehensively, or may even introduce new bugs. Instead, we propose property-based APR, which uses human-specified, program-independent and vulnerability-specific safety properties to derive source code patches for security vulnerabilities. Unlike properties that are approximated by observing the execution of test cases, such safety properties are precise and complete. The primary challenge lies in mapping such safety properties into source code patches that can be instantiated into an existing program. To address these challenges, we propose Senx, which, given a set of safety properties and a single input that triggers the vulnerability, detects the safety property violated by the vulnerability input and generates a corresponding patch that enforces the safety property and thus, removes the vulnerability. Senx solves several challenges with property-based APR: it identifies the program expressions and variables that must be evaluated to check safety properties and identifies the program scopes where they can be evaluated, it generates new code to selectively compute the values it needs if calling existing program code would cause unwanted side effects, and it uses a novel access range analysis technique to avoid placing patches inside loops where it could incur performance overhead. Our evaluation shows that the patches generated by Senx successfully fix 32 of 42 real-world vulnerabilities from 11 applications including various tools or libraries for manipulating graphics/media files, a programming language interpreter, a relational database engine, a collection of programming tools for creating and managing binary programs, and a collection of basic file, shell, and text manipulation tools.
2020-04-06
Guo, Haoran, Ai, Jun, Shi, Tao.  2019.  A Clone Code Detection Method Based on Software Complex Network. 2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). :120—121.

This paper introduces complex network into software clone detection and proposes a clone code detection method based on software complex network feature matching. This method has the following properties. It builds a software network model with many added features and codes written with different languages can be detected by a single method. It reduces the space of code comparison, and it searches similar subnetworks to detect clones without knowing any clone codes information. This method can be used in detecting open source code which has been reused in software for security analysis.

2020-03-23
Zheng, Yaowen, Song, Zhanwei, Sun, Yuyan, Cheng, Kai, Zhu, Hongsong, Sun, Limin.  2019.  An Efficient Greybox Fuzzing Scheme for Linux-based IoT Programs Through Binary Static Analysis. 2019 IEEE 38th International Performance Computing and Communications Conference (IPCCC). :1–8.

With the rapid growth of Linux-based IoT devices such as network cameras and routers, the security becomes a concern and many attacks utilize vulnerabilities to compromise the devices. It is crucial for researchers to find vulnerabilities in IoT systems before attackers. Fuzzing is an effective vulnerability discovery technique for traditional desktop programs, but could not be directly applied to Linux-based IoT programs due to the special execution environment requirement. In our paper, we propose an efficient greybox fuzzing scheme for Linux-based IoT programs which consist of two phases: binary static analysis and IoT program greybox fuzzing. The binary static analysis is to help generate useful inputs for efficient fuzzing. The IoT program greybox fuzzing is to reinforce the IoT firmware kernel greybox fuzzer to support IoT programs. We implement a prototype system and the evaluation results indicate that our system could automatically find vulnerabilities in real-world Linux-based IoT programs efficiently.

Naik, Nitin, Jenkins, Paul, Savage, Nick, Yang, Longzhi.  2019.  Cyberthreat Hunting - Part 1: Triaging Ransomware using Fuzzy Hashing, Import Hashing and YARA Rules. 2019 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE). :1–6.

Ransomware is currently one of the most significant cyberthreats to both national infrastructure and the individual, often requiring severe treatment as an antidote. Triaging ran-somware based on its similarity with well-known ransomware samples is an imperative preliminary step in preventing a ransomware pandemic. Selecting the most appropriate triaging method can improve the precision of further static and dynamic analysis in addition to saving significant t ime a nd e ffort. Currently, the most popular and proven triaging methods are fuzzy hashing, import hashing and YARA rules, which can ascertain whether, or to what degree, two ransomware samples are similar to each other. However, the mechanisms of these three methods are quite different and their comparative assessment is difficult. Therefore, this paper presents an evaluation of these three methods for triaging the four most pertinent ransomware categories WannaCry, Locky, Cerber and CryptoWall. It evaluates their triaging performance and run-time system performance, highlighting the limitations of each method.

2020-03-09
Nilizadeh, Shirin, Noller, Yannic, Pasareanu, Corina S..  2019.  DifFuzz: Differential Fuzzing for Side-Channel Analysis. 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). :176–187.
Side-channel attacks allow an adversary to uncover secret program data by observing the behavior of a program with respect to a resource, such as execution time, consumed memory or response size. Side-channel vulnerabilities are difficult to reason about as they involve analyzing the correlations between resource usage over multiple program paths. We present DifFuzz, a fuzzing-based approach for detecting side-channel vulnerabilities related to time and space. DifFuzz automatically detects these vulnerabilities by analyzing two versions of the program and using resource-guided heuristics to find inputs that maximize the difference in resource consumption between secret-dependent paths. The methodology of DifFuzz is general and can be applied to programs written in any language. For this paper, we present an implementation that targets analysis of Java programs, and uses and extends the Kelinci and AFL fuzzers. We evaluate DifFuzz on a large number of Java programs and demonstrate that it can reveal unknown side-channel vulnerabilities in popular applications. We also show that DifFuzz compares favorably against Blazer and Themis, two state-of-the-art analysis tools for finding side-channels in Java programs.
Li, Chi, Zhou, Min, Gu, Zuxing, Gu, Ming, Zhang, Hongyu.  2019.  Ares: Inferring Error Specifications through Static Analysis. 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). :1174–1177.
Misuse of APIs happens frequently due to misunderstanding of API semantics and lack of documentation. An important category of API-related defects is the error handling defects, which may result in security and reliability flaws. These defects can be detected with the help of static program analysis, provided that error specifications are known. The error specification of an API function indicates how the function can fail. Writing error specifications manually is time-consuming and tedious. Therefore, automatic inferring the error specification from API usage code is preferred. In this paper, we present Ares, a tool for automatic inferring error specifications for C code through static analysis. We employ multiple heuristics to identify error handling blocks and infer error specifications by analyzing the corresponding condition logic. Ares is evaluated on 19 real world projects, and the results reveal that Ares outperforms the state-of-the-art tool APEx by 37% in precision. Ares can also identify more error specifications than APEx. Moreover, the specifications inferred from Ares help find dozens of API-related bugs in well-known projects such as OpenSSL, among them 10 bugs are confirmed by developers. Video: https://youtu.be/nf1QnFAmu8Q. Repository: https://github.com/lc3412/Ares.
2020-02-17
Letychevskyi, Oleksandr, Peschanenko, Volodymyr, Radchenko, Viktor, Hryniuk, Yaroslav, Yakovlev, Viktor.  2019.  Algebraic Patterns of Vulnerabilities in Binary Code. 2019 10th International Conference on Dependable Systems, Services and Technologies (DESSERT). :70–73.
This paper presents an algebraic approach for formalizing and detecting vulnerabilities in binary code. It uses behaviour algebra equations for creating patterns of vulnerabilities and algebraic matching methods for vulnerability detection. Algebraic matching is based on symbolic modelling. This paper considers a known vulnerability, buffer overflow, as an example to demonstrate an algebraic approach for pattern creation.
2020-02-10
Izurieta, Clemente, Prouty, Mary.  2019.  Leveraging SecDevOps to Tackle the Technical Debt Associated with Cybersecurity Attack Tactics. 2019 IEEE/ACM International Conference on Technical Debt (TechDebt). :33–37.
Context: Managing technical debt (TD) associated with external cybersecurity attacks on an organization can significantly improve decisions made when prioritizing which security weaknesses require attention. Whilst source code vulnerabilities can be found using static analysis techniques, malicious external attacks expose the vulnerabilities of a system at runtime and can sometimes remain hidden for long periods of time. By mapping malicious attack tactics to the consequences of weaknesses (i.e. exploitable source code vulnerabilities) we can begin to understand and prioritize the refactoring of the source code vulnerabilities that cause the greatest amount of technical debt on a system. Goal: To establish an approach that maps common external attack tactics to system weaknesses. The consequences of a weakness associated with a specific attack technique can then be used to determine the technical debt principal of said violation; which can be measured in terms of loss of business rather than source code maintenance. Method: We present a position study that uses Jaccard similarity scoring to examine how 11 malicious attack tactics can relate to Common Weakness Enumerations (CWEs). Results: We conduct a study to simulate attacks, and generate dependency graphs between external attacks and the technical consequences associated with CWEs. Conclusion: The mapping of cyber security attacks to weaknesses allows operational staff (SecDevOps) to focus on deploying appropriate countermeasures and allows developers to focus on refactoring the vulnerabilities with the greatest potential for technical debt.
Yang, Jinqiu, Tan, Lin, Peyton, John, A Duer, Kristofer.  2019.  Towards Better Utilizing Static Application Security Testing. 2019 IEEE/ACM 41st International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP). :51–60.

Static application security testing (SAST) detects vulnerability warnings through static program analysis. Fixing the vulnerability warnings tremendously improves software quality. However, SAST has not been fully utilized by developers due to various reasons: difficulties in handling a large number of reported warnings, a high rate of false warnings, and lack of guidance in fixing the reported warnings. In this paper, we collaborated with security experts from a commercial SAST product and propose a set of approaches (Priv) to help developers better utilize SAST techniques. First, Priv identifies preferred fix locations for the detected vulnerability warnings, and group them based on the common fix locations. Priv also leverages visualization techniques so that developers can quickly investigate the warnings in groups and prioritize their quality-assurance effort. Second, Priv identifies actionable vulnerability warnings by removing SAST-specific false positives. Finally, Priv provides customized fix suggestions for vulnerability warnings. Our evaluation of Priv on six web applications highlights the accuracy and effectiveness of Priv. For 75.3% of the vulnerability warnings, the preferred fix locations found by Priv are identical to the ones annotated by security experts. The visualization based on shared preferred fix locations is useful for prioritizing quality-assurance efforts. Priv reduces the rate of SAST-specific false positives significantly. Finally, Priv is able to provide fully complete and correct fix suggestions for 75.6% of the evaluated warnings. Priv is well received by security experts and some features are already integrated into industrial practice.

Visalli, Nicholas, Deng, Lin, Al-Suwaida, Amro, Brown, Zachary, Joshi, Manish, Wei, Bingyang.  2019.  Towards Automated Security Vulnerability and Software Defect Localization. 2019 IEEE 17th International Conference on Software Engineering Research, Management and Applications (SERA). :90–93.

Security vulnerabilities and software defects are prevalent in software systems, threatening every aspect of cyberspace. The complexity of modern software makes it hard to secure systems. Security vulnerabilities and software defects become a major target of cyberattacks which can lead to significant consequences. Manual identification of vulnerabilities and defects in software systems is very time-consuming and tedious. Many tools have been designed to help analyze software systems and to discover vulnerabilities and defects. However, these tools tend to miss various types of bugs. The bugs that are not caught by these tools usually include vulnerabilities and defects that are too complicated to find or do not fall inside of an existing rule-set for identification. It was hypothesized that these undiscovered vulnerabilities and defects do not occur randomly, rather, they share certain common characteristics. A methodology was proposed to detect the probability of a bug existing in a code structure. We used a comprehensive experimental evaluation to assess the methodology and report our findings.

Talukder, Md Arabin Islam, Shahriar, Hossain, Qian, Kai, Rahman, Mohammad, Ahamed, Sheikh, Wu, Fan, Agu, Emmanuel.  2019.  DroidPatrol: A Static Analysis Plugin For Secure Mobile Software Development. 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC). 1:565–569.

While the number of mobile applications are rapidly growing, these applications are often coming with numerous security flaws due to the lack of appropriate coding practices. Security issues must be addressed earlier in the development lifecycle rather than fixing them after the attacks because the damage might already be extensive. Early elimination of possible security vulnerabilities will help us increase the security of our software and mitigate or reduce the potential damages through data losses or service disruptions caused by malicious attacks. However, many software developers lack necessary security knowledge and skills required at the development stage, and Secure Mobile Software Development (SMSD) is not yet well represented in academia and industry. In this paper, we present a static analysis-based security analysis approach through design and implementation of a plugin for Android Development Studio, namely DroidPatrol. The proposed plugins can support developers by providing list of potential vulnerabilities early.

Rahman, Md Rayhanur, Rahman, Akond, Williams, Laurie.  2019.  Share, But Be Aware: Security Smells in Python Gists. 2019 IEEE International Conference on Software Maintenance and Evolution (ICSME). :536–540.

Github Gist is a service provided by Github which is used by developers to share code snippets. While sharing, developers may inadvertently introduce security smells in code snippets as well, such as hard-coded passwords. Security smells are recurrent coding patterns that are indicative of security weaknesses, which could potentially lead to security breaches. The goal of this paper is to help software practitioners avoid insecure coding practices through an empirical study of security smells in publicly-available GitHub Gists. Through static analysis, we found 13 types of security smells with 4,403 occurrences in 5,822 publicly-available Python Gists. 1,817 of those Gists, which is around 31%, have at least one security smell including 689 instances of hard-coded secrets. We also found no significance relation between the presence of these security smells and the reputation of the Gist author. Based on our findings, we advocate for increased awareness and rigorous code review efforts related to software security for Github Gists so that propagation of insecure coding practices are mitigated.

Rahman, Akond, Parnin, Chris, Williams, Laurie.  2019.  The Seven Sins: Security Smells in Infrastructure as Code Scripts. 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). :164–175.

Practitioners use infrastructure as code (IaC) scripts to provision servers and development environments. While developing IaC scripts, practitioners may inadvertently introduce security smells. Security smells are recurring coding patterns that are indicative of security weakness and can potentially lead to security breaches. The goal of this paper is to help practitioners avoid insecure coding practices while developing infrastructure as code (IaC) scripts through an empirical study of security smells in IaC scripts. We apply qualitative analysis on 1,726 IaC scripts to identify seven security smells. Next, we implement and validate a static analysis tool called Security Linter for Infrastructure as Code scripts (SLIC) to identify the occurrence of each smell in 15,232 IaC scripts collected from 293 open source repositories. We identify 21,201 occurrences of security smells that include 1,326 occurrences of hard-coded passwords. We submitted bug reports for 1,000 randomly-selected security smell occurrences. We obtain 212 responses to these bug reports, of which 148 occurrences were accepted by the development teams to be fixed. We observe security smells can have a long lifetime, e.g., a hard-coded secret can persist for as long as 98 months, with a median lifetime of 20 months.

Cheng, Xiao, Wang, Haoyu, Hua, Jiayi, Zhang, Miao, Xu, Guoai, Yi, Li, Sui, Yulei.  2019.  Static Detection of Control-Flow-Related Vulnerabilities Using Graph Embedding. 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS). :41–50.

Static vulnerability detection has shown its effectiveness in detecting well-defined low-level memory errors. However, high-level control-flow related (CFR) vulnerabilities, such as insufficient control flow management (CWE-691), business logic errors (CWE-840), and program behavioral problems (CWE-438), which are often caused by a wide variety of bad programming practices, posing a great challenge for existing general static analysis solutions. This paper presents a new deep-learning-based graph embedding approach to accurate detection of CFR vulnerabilities. Our approach makes a new attempt by applying a recent graph convolutional network to embed code fragments in a compact and low-dimensional representation that preserves high-level control-flow information of a vulnerable program. We have conducted our experiments using 8,368 real-world vulnerable programs by comparing our approach with several traditional static vulnerability detectors and state-of-the-art machine-learning-based approaches. The experimental results show the effectiveness of our approach in terms of both accuracy and recall. Our research has shed light on the promising direction of combining program analysis with deep learning techniques to address the general static analysis challenges.

Ashfaq, Qirat, Khan, Rimsha, Farooq, Sehrish.  2019.  A Comparative Analysis of Static Code Analysis Tools That Check Java Code Adherence to Java Coding Standards. 2019 2nd International Conference on Communication, Computing and Digital Systems (C-CODE). :98–103.

Java programming language is considered highly important due to its extensive use in the development of web, desktop as well as handheld devices applications. Implementing Java Coding standards on Java code has great importance as it creates consistency and as a result better development and maintenance. Finding bugs and standard's violations is important at an early stage of software development than at a later stage when the change becomes impossible or too expensive. In the paper, some tools and research work done on Coding Standard Analyzers is reviewed. These tools are categorized based on the type of rules they cheeked, namely: style, concurrency, exceptions, and quality, security, dependency and general methods of static code analysis. Finally, list of Java Coding Standards Enforcing Tools are analyzed against certain predefined parameters that are limited by the scope of research paper under study. This review will provide the basis for selecting a static code analysis tool that enforce International Java Coding Standards such as the Rule of Ten and the JPL Coding Standards. Such tools have great importance especially in the development of mission/safety critical system. This work can be very useful for developers in selecting a good tool for Java code analysis, according to their requirements.

2020-01-27
Schmeidl, Florian, Nazzal, Bara, Alalfi, Manar H..  2019.  Security Analysis for SmartThings IoT Applications. 2019 IEEE/ACM 6th International Conference on Mobile Software Engineering and Systems (MOBILESoft). :25–29.
This paper presents a fully automated static analysis approach and a tool, Taint-Things, for the identification of tainted flows in SmartThings IoT apps. Taint-Things accurately identified all tainted flows reported by one of the state-of the-art tools with at least 4 times improved performance. In addition, our approach reports potential vulnerable tainted flow in a form of a concise security slice, which could provide security auditors with an effective and precise tool to pinpoint security issues in SmartThings apps under test.
2020-01-20
Zhu, Lipeng, Fu, Xiaotong, Yao, Yao, Zhang, Yuqing, Wang, He.  2019.  FIoT: Detecting the Memory Corruption in Lightweight IoT Device Firmware. 2019 18th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/13th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :248–255.
The IoT industry has developed rapidly in recent years, which has attracted the attention of security researchers. However, the researchers are hampered by the wide variety of IoT device operating systems and their hardware architectures. Especially for the lightweight IoT devices, many manufacturers do not provide the device firmware images, embedded firmware source code or even the develop documents. As a result, it hinders traditional static analysis and dynamic analysis techniques. In this paper, we propose a novel dynamic analysis framework, called FIoT, which aims at finding memory corruption vulnerabilities in lightweight IoT device firmware images. The key idea is dynamically run the binary code snippets through symbolic execution with carrying out a fuzzing test. Specifically, we generate code snippets through traversing the control-flow graph (CFG) in a backward manner. We improved the CFG recovery approach and backward slice approach for better performance. To reduce the influence of the binary firmware, FIoT leverages loading address determination analysis and library function identification approach. We have implemented a prototype of FIoT and conducted experiments. Our results show that FIoT can complete the Fuzzing test within 40 seconds in average. Considering 170 seconds for static analysis, FIoT can load and analyze a lightweight IoT firmware within 210 seconds in total. Furthermore, we illustrate the effectiveness of FIoT by applying it over 115 firmware images from 17 manufacturers. We have found 35 images exist memory corruptions, which are all zero-day vulnerabilities.
2019-12-17
Huang, Jeff.  2018.  UFO: Predictive Concurrency Use-After-Free Detection. 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE). :609-619.

Use-After-Free (UAF) vulnerabilities are caused by the program operating on a dangling pointer and can be exploited to compromise critical software systems. While there have been many tools to mitigate UAF vulnerabilities, UAF remains one of the most common attack vectors. UAF is particularly di cult to detect in concurrent programs, in which a UAF may only occur with rare thread schedules. In this paper, we present a novel technique, UFO, that can precisely predict UAFs based on a single observed execution trace with a provably higher detection capability than existing techniques with no false positives. The key technical advancement of UFO is an extended maximal thread causality model that captures the largest possible set of feasible traces that can be inferred from a given multithreaded execution trace. By formulating UAF detection as a constraint solving problem atop this model, we can explore a much larger thread scheduling space than classical happens-before based techniques. We have evaluated UFO on several real-world large complex C/C++ programs including Chromium and FireFox. UFO scales to real-world systems with hundreds of millions of events in their execution and has detected a large number of real concurrency UAFs.

2019-12-02
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.