Abstract:Preface to Special Issue on System Software Security

Abstract:Software verification has always been a popular research topic to ensure the correctness and security of software. However, due to the complex semantics and syntax of programming languages, the formal methods for verifying the correctness of programs have the problems of low accuracy and low efficiency. In particular, the state change in address space caused by pointer operations makes it difficult to guarantee the verification accuracy of existing model checking methods. By combining model checking and sparse value-flow analysis, this paper designs a spatial flow model to effectively describe the state behavior of C code at the symbolic-variable level and address-space level and proposes a model checking algorithm of CounterExample-Guided Abstraction refinement and Sparse value-flow strong update (CEGAS), which enables points-to-sensitive formal verification for C code. This paper establishes a C-code benchmark containing a variety of pointer operations and conducts comparative experiments on the basis of this benchmark. These experiments indicate that in the task of analyzing multi-class C code features, the model checking algorithm CEGAS proposed in this paper can achieve outstanding results compared with the existing model checking tools. The verification accuracy of CEGAS is 92.9%, and the average verification time of each line of code is 2.58 ms, both of which are better than those of existing verification tools.

Abstract:Trusted Execution Environment (TEE) is an architectural solution for secure computing that requires confidentiality and integrity for private data and code. In recent years, TEE has become the research hotspot for machine learning privacy protection, encrypted database, blockchain security, etc. This paper addresses the performance problem of the system under this new trusted hardware. We analyze the performance of the new trusted hardware, i.e., Intel SGXv2. We find that the paging overhead in SGXv1 is no longer the main issue in SGXv2 under the premise of configuring large secure memory. However, the setup of large secure memory leads to two new problems. First, the available range of normal memory is narrowed down, which increases the memory pressure of normal applications, especially big data applications. Second, secure memory is usually underutilized, resulting in low overall physical memory utilization. To solve the above problems, this paper proposes a new lightweight code migration approach, which dynamically migrates the code of normal applications into secure memory, while leaving the data in place. The migrated code can use secure memory and avoid the drastic performance degradation caused by disk swapping. Experimental results show that the proposed approach can reduce the runtime overhead of normal applications by 73.2\% to 98.7\% without affecting the isolation and the use of secure applications.

Abstract:Reference counting (refcount) is a common memory management technique in modern software. Refcount errors can often lead to severe memory errors such as memory leak and use-after-free. Many efforts to harden refcount security rely on known refcount fields as their input. However, due to the complexity of software code, identifying refcount fields in source code is very challenging. Traditional methods of identifying refcount fields are mainly based on code pattern matching and have great limitations such as requiring expert experience to summarize code patterns, which is a laborious job. Besides, the manually summarized patterns do not cover all cases, resulting in low recall rate. To address these problems, this paper proposes to characterize a field based on the field name and the code behavior associated with the field and designs a multimodal deep learning based approach. The paper implements a prototype of the new approach for Linux kernel code. In the evaluation, the precision and recall rate achieved by the prototype system are 96.98% and 93.54%, respectively. In contrast, the traditional identification method based on code pattern matching did not report any refcount fields on the testing set. In addition, we identify 61 refcount fields which are implemented with insecure data types in the latest Linux kernel. Until now, we have reported 21 of them to the Linux community, of which six have been confirmed.

Abstract:Automatic Exploit Generation (AEG) has become one of the most important ways to demonstrate the exploitability of vulnerabilities. However, state-of-the-art AEG solutions in general assume the target system has no mitigations deployed, which is not true in modern operating systems since they often deploy mitigations like Data Execution Prevention (DEP) and Address Space Layout Randomization (ASLR). This paper presents the automatic solution EoLeak that can exploit heap vulnerabilities to leak sensitive data and bypass ASLR and DEP at the same time. At a high level, EoLeak analyzes the program execution trace of the Proof-Of-Concept (POC) input that triggers the heap vulnerabilities, characterizes the memory profile from the trace, locates sensitive data (e.g., code pointers), constructs leakage primitives that disclose sensitive data, and generates exploits for the entire process when possible. We have implemented a prototype of EoLeak and evaluated it on a set of Capture The Flag (CTF) binary programs and several real-world applications. Evaluation results reveal that EoLeak is effective at leaking data and generating exploits.