JavaScript is increasingly being deployed as binaries in security-critical embedded domains, such as IoT devices, edge computing, and intelligent vehicle platforms. This widespread adoption highlights the importance of dynamic analysis to ensure the security of JavaScript applications, particularly at the bytecode level. However, existing dynamic analysis techniques often rely on static instrumentation, which significantly increases of the executable size. This, in turn, leads to higher memory consumption and performance degradation-issues that are especially problematic in resource-constrained environments. In this paper, we present the first dynamic analysis approach for JavaScript bytecode that leverages load-time instrumentation to address this issue. We begin by designing a custom intermediate representation (IR) for JavaScript bytecode constructed at load time. We then develop a set of lowlevel hooks that are triggered at key points in the program execution flow. In addition, we introduce a set of flexible APIs to support customized instrumentation and dynamic analyses. We implement a software prototype, JasLoad, and conduct extensive evaluations. Evaluation results demonstrate that our approach significantly enhances the efficiency and effectiveness of dynamic analysis on resource-constrained devices. By combining JasLoad's bytecode loading/unloading with adaptive instrumentation, we reduce runtime overhead by up to 70.53 % and decrease code size expansion under full instrumentation from 603.68 % to 144.25 %, compared to prior JavaScript bytecode analysis methods.

Rust emerges as a promising safe language and is gaining rapid adoption in security-critical domains. However, Rust programs are susceptible to memory and thread safety issues, making dynamically analyzing Rust issues imperative. Unfortunately, a dynamic analysis framework for Rust is still lacking, hampering the advancement of dynamic analysis for Rust and posing security risks for the language.In this paper, we present RuDyna, the first Rust native dynamic analysis framework to the best of our knowledge. Our framework aims to instrument Rust programs and provide a set of hooks for monitoring runtime events. To this end, we first propose instrumenting the Rust MIR with three rules designed for satisfying its constraints. We then present four instrument strategies to inject various runtime events on MIR. Finally, we develop a hierarchical strategy to instrument configurable hooks to reduce overheads. We implement RuDyna by extending Rust’s official rustc compiler and hooks are provided as a Rust library. We conduct evaluation on a set of micro-benchmarks and 4 real-world large Rust projects. Experimental results indicate that RuDyna preserves the original semantics of programs, with an acceptable runtime overhead ranging from 1.1 × to 3.6 ×, which aligns with built-in instrumentation in rustc and similar frameworks for other languages. Moreover, we implement six analyses based on RuDyna, demonstrating its practical usability.

JavaScript is rapidly being deployed in security-critical embedded domains, including IoT devices, edge computing, and smart automotive applications. Embedded JavaScript virtual machines (VMs) are critical in powering such deployments, which should be secure and trustworthy. Fuzzing is an effective approach in detecting deep bugs in these VMs by generating diverse VM bytecode programs. However, existing JavaScript fuzzers are still limited in generating diverse and valid bytecode that finds deep bugs, because they fail to track the VM operand-stack state, which leads to invalid programs and missed bugs.In this paper, we present a novel fuzzing approach called DFAFuzz, to detect deep bugs in embedded JavaScript VMs. Our key idea is to use a type-directed deterministic finite automaton (DFA) to track instruction type information, guiding the generation of new type-correct JavaScript bytecode programs from existing fuzzing seeds. First, our approach employs type reconstruction to track variable type changes during bytecode generation. Second, our approach utilizes type transitions with the aid of DFA to guide bytecode generation to produce valid bytecode. We implement a software prototype DFAFuzzer and conduct extensive experiments to evaluate its effectiveness on JerryScript and QuickJS. Our results show that DFAFuzzer improves the bytecode validity ratio by 7.6% and 2.8% for JerryScript and QuickJS over AFL++, respectively. Furthermore, DFAFuzzer detects 111 bugs that are missed by state-of-the-art fuzzers, AFL++ and Fuzzilli.

Rust has emerged as a highly promising systems programming language for security-critical applications, owing to its strong type system and ownership model, which effectively prevent memory safety issues. However, real-world Rust applications are often multilingual and must interact with external modules written in memory-unsafe languages (e.g., C/C++) through foreign function interface (FFI). These interactions require integrating disparate memory management mechanisms and typically bypass Rust’s compiler safety checks, making them highly error-prone. Consequently, this may introduce memory safety issues, thereby compromising Rust’s memory safety guarantees.In this paper, we propose Rusty, a technique that enables cross-language static analysis to effectively detect memory safety bugs in multilingual Rust programs. Specifically, we first convert Rust and other languages into a unified intermediate representation to overcome language heterogeneity. Second, we employ value-flow analysis to perform program slicing, establishing a precise analysis scope. Building upon these foundations, we develop context-sensitive interprocedural abstract interpretation combined with points-to analysis to effectively identify memory safety bugs in multilingual interactions. We implemented a prototype of Rusty and conducted extensive experiments to evaluate its practical effectiveness and performance using both micro-benchmarks and real-world CWEs. The experimental results demonstrate that Rusty can effectively detect memory bugs in multilingual Rust programs while maintaining favorable detection efficiency and resource overhead.

Deep learning libraries such as PyTorch and TensorFlow are essential for building security-critical downstream deep learning applications. Bugs in these libraries compromise their correctness, robustness, and security, thereby undermining the reliability of downstream applications. Unfortunately, effectively detecting bugs in deep learning library remains challenging, as existing approaches often fail to generate effective test cases due to their inability to synthesize complex input constraints that govern deep learning library functions.In this paper, we present DeepLancet, the first approach for effectively detecting deep learning library bugs by leveraging large language models (LLMs) to systematically parse documentation and thereby assist in the generation of high-quality test cases. Our key observation is that mainstream deep learning libraries typically provide comprehensive and well-structured documentation, which contains detailed descriptions of input constraints that we can effectively synthesize and leverage to generate syntactically valid and semantically correct test cases. Specifically, we first synthesize function constraint descriptions from the documentation by leveraging LLMs. We then generate rigorous constraints which are leveraged to generate test cases through an attribution-based approach in Python. Finally, we employ a differential testing approach on CPU and GPU to detect bugs. We build a software prototype for DeepLancet, and our evaluation results demonstrate that DeepLancet is effective in uncovering previously unknown real-world bugs: it successfully uncovers 20 bugs in the latest release of PyTorch, including 7 previously unknown ones. Moreover, we compare DeepLancet with DocTer, a state-of-the-art technique that also leverages documentation for constraint extraction, and the results indicate that DeepLancet can extract more comprehensive constraints, thereby uncovering 3 more bugs that were missed by DocTer.

Rust is a promising systems programming language that provides strong security guarantees without sacrificing efficiency. To fully exploit Rust’s security benefits, transpilation is essential to migrate legacy C code to Rust. However, existing studies and practical transpilers all assumed that transpiled Rust programs are more secure and trustworthy than the corresponding C sources. Unfortunately, whether such an assumption truly holds in practice is still unknown. Therefore, a systematic empirical security investigation is urgently needed to evaluate the security risks and implications of C-to-Rust transpilations. In this paper, to fill this gap, we take the first step towards investigating the security risks of transpiled Rust code. To this end, we first create a dataset comprising 25,183 vulnerable C programs, to systematically examine how known vulnerabilities manifest after the transpilation. We then conduct an empirical study of the generated Rust transpiled from the C dataset, and obtain important findings and insights from the results: 1) we find that Rust’s built-in checks detect 14,201 vulnerabilities (56.4%) in C2Rust translations and 15,718 (62.4%) in GPT-4 translations, 2) we identify three root causes of semantic correction, behavioral masking, and latent unsafe preservation, leading to detection failures, and 3) we confirm that safety tools like ASan and TSan enhance vulnerability detection in Rust up to 26%. We suggest that: 1) researchers should improve comprehension of Rust security and conduct future research on code transpilation, 2) toolchain builders should refine transpilation approaches to better improve security of transpiled code, and 3) developers should employ security tools to mitigate potential security risks. We believe these findings and suggestions will help researchers, toolchain builders, and developers, by providing better guidelines for code transpilation and Rust security in general.

Deep learning compilers are essential for deploying deep learning applications across heterogeneous hardware platforms. To improve execution efficiency, they employ sophisticated optimizations, which inevitably introduce bugs due to their considerably large code size and complex logic. Therefore, effectively detecting optimization bugs is essential to guarantee the correctness and trustworthiness of deep learning compilers.In this paper, we present ORThrus, an automatic approach to effectively detect optimization bugs in deep learning compilers. Conceptually, our approach develops a non-optimizing reference compiler to an optimizing compiler, then to detect optimization bugs by comparing the discrepancies in the two compilers’ outputs. Obtaining a non-optimizing reference compiler is challenging, because existing deep learning compilers provide limited control over optimizations. We thus propose a novel approach dubbed optimization resistance transformation that structurally transforms an input deep learning model from an optimizable form to an unoptimizable form that the deep learning compiler can no longer perform the potential optimizations. We build a prototype for our approach and evaluate it in an extensive testing campaign on two widely-used deep learning compilers TVM and ONNXRuntime. ORThrus detects 21 bugs, of which 9 are non-crash optimization bugs and 1 is missed by the state-of-the-art tool NNSmith even with its cross reference feature enabled. Meanwhile, ORThrus introduces negligible execution overhead.

Transformers, renowned for their powerful feature extraction capabilities, have played an increasingly prominent role in various vision tasks. Especially, recent advancements present transformer with hierarchical structures such as Dilated Neighborhood Attention Transformer (DiNAT), demonstrating outstanding ability to efficiently capture both global and local features. However, transformers’ application in edge detection has not been fully exploited. In this paper, we propose EdgeNAT, a one-stage transformer-based edge detector with DiNAT as the encoder, capable of extracting object boundaries and meaningful edges both accurately and efficiently. On the one hand, EdgeNAT captures global contextual information and detailed local cues with DiNAT, on the other hand, it enhances feature representation with a novel SCAF-MLA decoder by utilizing both inter-spatial and inter-channel relationships of feature maps. Extensive experiments on multiple datasets show that our method achieves state-of-the-art performance on both RGB and depth images. Notably, on the widely used BSDS500 dataset, our L model achieves impressive performances, with ODS F-measure and OIS F-measure of 86.0%, 87.6% for multi-scale input,and 84.9%, and 86.3% for single-scale input, surpassing the current state-of-the-art EDTER by 1.2%, 1.1%, 1.7%, and 1.6%, respectively. Moreover, as for throughput, our approach runs at 20.87 FPS on RTX 4090 GPU with single-scale input. Code: https://github.com/jhjie/EdgeNAT.

Edge detection is a core component in a wide range of vision tasks, and is expected to be both efficient and accurate to identify boundaries and edges in images. And it has been a hot research field for long period. Currently, vision transformers are playing an increasingly prominent role in various downstream tasks, and the SOTA edge detector EDTER employs vision transformer as its encoder. However, ViTs are also known for their computational burden due to the large amount of parameters, leading to higher processing latency than lightweight CNNs. Recently, EfficientFormerV2, which has a novel network with low latency and high parameter efficiency, has proved that transformer-based network could outperform CNN-based network in both accuracy and efficiency. Inspired by this architecture, this paper proposes a novel edge detector EFED with EfficientFormerV2 as the encoder, and an efficient Multi-Level Aggregation decoder SMLA to extract both local and global features. Extensive experiments are conducted on two widely employed datasets, BSDS500 and NYUDv2, demonstrating that compared with EDTER, our detector not only improves the throughput by 10 times, but also achieves competitive accuracy. With single scale input on BSDS500 dataset, our EFED model achieves ODS F-measure and OIS F-measure of 82.4% and 84.2%, while for EDTER the corresponding values are 82.4% and 84.1%, respectively.

WebAssembly (Wasm) is an emerging binary instruction set architecture designed for secure binary program execution and is rapidly being deployed across various security-critical domains, such as edge computing and smart contracts. However, despite its security-oriented design, Wasm remains susceptible to vulnerabilities, including integer overflows and memory corruption, due to the lack of effective protection mechanisms, which undermines its security guarantees.In this paper, we present WaShadow, the first approach for effective Wasm protection using virtual machine-aware shadow memory. Our key insight is that, since Wasm is a virtual instruction set, we can leverage memory layout information in the underlying Wasm VMs to enforce the protection. Specifically, we first extend the Wasm VMs with shadow memory to record memory information and track the status of linear memory, by introducing two new pseudo Wasm instructions for inserting and performing sanity checks on canaries in the linear memory. We then design a static binary instrumentation method to instrument Wasm binaries with canary instructions. Finally, we implement these canary pseudo-instructions through virtual machine extensions as well as a set of vulnerability detection algorithms as security plugins. We implemented a software prototype for WaShadow and conducted extensive experiments to evaluate its effectiveness, usability, and overhead on micro and real-world benchmarks. Experimental results demonstrated that WaShadow is effective in protecting Wasm linear memory against various memory vulnerabilities, with an average code size increase of 26.5% and an execution time penalty of 108.5%.

JavaScript is rapidly being deployed as binaries in security-critical embedded domains, including IoT devices, edge computing, and smart automotive applications. Ensuring the security of JavaScript binaries in these domains necessitates comprehensive binary code analysis. However, despite the urgent need, a universal approach to analyzing JavaScript binaries is lacking due to the bytecode heterogeneity across the various JavaScript virtual machines.In this paper, to fill this gap, we present the first grammar-free, universal program analysis approach tailored for JavaScript binaries. We first design a syntax-independent intermediate representation called JasByte to encode diverse JavaScript binaries. We then develop a universal translator equipped with a set of APIs to transform JavaScript binaries into JasByte. We design a suit of program analysis algorithms for error detection, debugging, and fuzzing, to identify bugs in JavaScript VMs. We design and implement a software prototype JasFree and conduct extensive evaluations. Our results show that JasFree effectively enables construction of diverse static and dynamic analysis by reducing the overhead from 660.38% to 290.84%, outperforming the state-of-the-art tool Jalangi2. Moreover, JAS-FREE facilitates effective mutation of JasByte, resulting in the detection of 25 new vulnerabilities, all of which were missed by existing methods.

Safe binary execution is often a crucial requirement in today's security critical computing infrastructures. WebAssembly is an emerging language designed for safe binary execution that has been deployed in many security critical domains, such as blockchain, edge computing, and clouds. However, WebAssembly's security guarantee is not a cure-all, and recent studies have revealed a large spectrum of security issues such as integer overflows and memory vulnerabilities, leading to serious security hazards to WebAssembly applications. In this paper, we propose the first automated bug detection framework for WebAssembly programs based on dynamic program analysis, directly on WebAssembly binaries. To realize the whole process, we present WASMDYPA, the dynamic bug detection system, consisting of three primary components: 1) an input generator for WebAssembly binaries; 2) a static instrumentation hook providing extensible interfaces to collect runtime information; and 3) dynamic program analysis algorithms as security plugins to detect vulnerabilities. We have implemented a software prototype for WASMDYPA, and have conducted experiments to evaluate the effectiveness, usefulness, performance and overhead of our approach. Experimental results demonstrated that WASMDyPA can accurately detect vulnerabilities with a 88.24% precision and a 93.75% recall. Furthermore, WAS-MDyPA detected 56 bugs in real-world WebAssembly programs, including 2 integer overflows and 54 memory bugs.

Profile-Guided Optimization (PGO) is a novel compiler optimization leveraging runtime feedback and has been applied successfully to optimize Android kernels gaining significant performance improvements. However, current studies as well as implementations of PGO-based Android kernel optimizations still suffer from three problems: 1) optimization inflexibility due to restricted algorithms for generating profiles and for simulating real-world usage scenarios; 2) considerable optimization efforts due to the extensive manual interventions needed; and 3) optimization failures due to kernel version fragmentation.This paper presents MePof, the first modular and end-to-end PGO framework for Android kernels. The MePof framework consists of three key components: 1) a tool orchestration, that integrates two novel algorithms for generating profiles, and three methods for simulating real-world scenarios that can be flexibly switched according to the usage scenario; 2) a domain-specific language (DSL) that can specify PGO-based optimization strategies and a corresponding compiler translating the DSL programs into configuration files necessary for optimization; and 3) an adapter that automatically triggers and completes the optimization when the Android kernel version changes.We have implemented a prototype for MePof and have conducted extensive experiments to evaluate its effectiveness, performance, and usability. Experimental results demonstrated that: 1) MePof is effective, with performance improvement 9.39% on average; 2) MePof is efficient by saving up to 39.07% of time than manual optimizations; and 3) MePof is highly usable by requiring only one manual intervention instead of more than 30 manual interventions as in the existing optimization framework.

Despite the fact that Rust is designed to be a secure programming language for system programming, it is still vulnerable and exploitable due to its inclusion of an unsafe sub-language. However, existing studies on Rust security only focus on static detection or rectification of vulnerability, but ignore the problem of timely and effective rectifications of vulnerabilities dynamically. In this paper, to fill this gap, we present RUSPATCH, the first infrastructure to timely and effectively patch vulnerable Rust applications. RUSPATCH consists of two main phases: static partitioning and dynamic patching. In the static partitioning phase, RUSPATCH divides the candidate program into target code and patch candidates via a customized compiler. During the patching phase, RUSPATCH dynamically validates and applies the security patch once a vulnerability is detected. To realize the whole process, we tackled three technical challenges of language discrepancy, efficiency issues, and security threats. We have designed and implemented a software prototype for RUSPATCH, and have conducted extensive experiments to evaluate its effectiveness, performance, overhead, and usefulness. Experimental results demonstrated that RusPATCH is effective in patching off-the-shelf Rust applications including real-world Rust CVEs, and the extra overhead RusPATCH introduced is less than 3.28% and thus insignificant. Furthermore, RUSPATCH is easy to incorporate into existing Rust applications without any manual interventions.

WebAssembly is an emerging secure programming language and portable instruction set architecture, and has been deployed in diverse security-critical scenarios due to its safety advantages. However, WebAssembly’s linear memory is still vulnerable to buffer overflows due to the lack of effective protection mechanism, defeating its security guarantees. In this paper, we present VMCanary, the first framework for effective WebAssembly memory protection, by leveraging a canary approach but with the aid from WebAssembly virtual machines (VMs). Our key idea is that, due to the fact that WebAssembly is a managed programming language to be executed by underlying WebAssembly VMs, the VMs must understand any protection mechanisms already enforced in programs. With this key idea, we first propose the concept of canary in code, which is like a traditional canary in data but whose semantics is understandable by underlying WebAssembly VMs. To realize this kind of canary, we introduced two novel WebAssembly instructions by defining their semantics. Furthermore, we designed an instrumentation for WebAssembly binaries to instrument these two instructions automatically, hence no sources and compiler toolchain modifications are required. We have implemented a software prototype for VMCanary, and have conducted extensive experiment to evaluate it on micro benchmarks and 59 real-world CWEs. Experimental results demonstrated that VMCanary is effective in protecting Wasm memory with negligible overhead (3% on average).

Python, as one of the most popular and important programming languages in the era of data science, has recently introduced a syntax for static type annotations with PEP 484, to improve code maintainability, quality, and readability. However, it is still unknown whether and how static type annotations are used in practical Python projects.This paper presents, to the best of our knowledge, the first and most comprehensive empirical study on the defects, evolution and rectification of static type annotations in Python projects. We first designed and implemented a software prototype dubbed PYSCAN, then used it to scan notable Python projects with diverse domains and sizes and type annotation manners, which add up to 19,478,428 lines of Python code. The empirical results provide interesting findings and insights, such as: 1) we proposed a taxonomy of Python type annotation-related defects, by classifying defects into four categories; 2) we investigated the evolution of type annotation-related defects; and 3) we proposed automatic defect rectification strategies, generating rectification suggestions for 82 out of 110 (74.55%) defects successfully. We suggest that: 1) Python language designers should clarify the type annotation specification; 2) checking tool builders should improve their tools to suppress false positives; and 3) Python developers should integrate such checking tools into their development workflow to catch type annotation-related defects at an early development stage.We have reported our findings and suggestions to Python language designers, checking tool builders, and Python developers. They have acknowledged us and taken actions based on our suggestions. We believe these guidelines would improve static type annotation practices and benefit the Python ecosystem in general.

Smart contract decompilers, converting smart contract bytecode into smart contract source code, have been used extensively in many scenarios such as binary code analysis, reverse engineering, and security studies. However, existing studies, as well as industrial engineering practices, all assumed that smart contract decompilers are reliable and trustworthy, to generate correct and semantically equivalent source code from binaries. Unfortunately, whether such an assumption truly holds in practice is still unknown.In this paper, we conduct, to the best of our knowledge, the first and most comprehensive large-scale empirical study of smart contract decompilers, to gain an understanding of the reliability, limitations, and remaining research challenges of state-of-the-art smart contract decompilation tools. We first designed and implemented a software prototype SOLINSIGHT, then used it to study 5 state-of-the-art smart contract decompilers. We obtained important findings and insights from empirical results, such as: 1) we proposed 3 root causes leading to decompiler failures; 2) we revealed 2 reasons hurting performance; 3) we identified 3 root causes affecting decompilation effectiveness; 4) we proposed a measurement metric for completeness; and 5) we investigated the resilience of contract decompilers against program transformations. We suggest that: 1) decompiler builders should enhance decompilers in terms of effectiveness, performance, and completeness; and 2) security researchers should select appropriate decompilers based on the suggestions in this study. We believe these findings and suggestions will help decompiler builders, contract developers, and security researchers, by providing better guidelines for contract decompiler studies.

Python continues to be one of the most popular programming languages and has been used in many safety-critical fields such as medical treatment, autonomous driving systems, and data science. These fields put forward higher security requirements to Python ecosystems. However, existing studies on machine learning systems in Python concentrate on data security, model security and model privacy, and just assume the underlying Python virtual machines (PVMs) are secure and trustworthy. Unfortunately, whether such an assumption really holds is still unknown.This paper presents, to the best of our knowledge, the first and most comprehensive empirical study on the security of CPython, the official and most deployed Python virtual machine. To this end, we first designed and implemented a software prototype dubbed PVMSCAN, then use it to scan the source code of the latest CPython (version 3.10) and other 10 versions (3.0 to 3.9), which consists of 3,838,606 lines of source code. Empirical results give relevant findings and insights towards the security of Python virtual machines, such as: 1) CPython virtual machines are still vulnerable, for example, PVMSCAN detected 239 vulnerabilities in version 3.10, including 55 null dereferences, 86 uninitialized variables and 98 dead stores; Python/C API-related vulnerabilities are very common and have become one of the most severe threats to the security of PVMs: for example, 70 Python/C API-related vulnerabilities are identified in CPython 3.10; 3) the overall quality of the code remained stable during the evolution of Python VMs with vulnerabilities per thousand line (VPTL) to be 0.50; and 4) automatic vulnerability rectification is effective: 166 out of 239 (69.46%) vulnerabilities can be rectified by a simple yet effective syntax-directed heuristics.We have reported our empirical results to the developers of CPython, and they have acknowledged us and already confirmed and fixed 2 bugs (as of this writing) while others are still being analyzed. This study not only demonstrates the effectiveness of our approach, but also highlights the need to improve the reliability of infrastructures like Python virtual machines by leveraging state-of-the-art security techniques and tools.

Rust is an emerging programming language designed for secure system programming that provides both security guarantees and runtime efficiency and has been increasingly used to build software infrastructures such as OS kernels, web browsers, databases, and blockchains. To support arbitrary low-level programming and to provide more flexibility, Rust introduced the unsafe feature, which may lead to security issues such as memory or concurrency vulnerabilities. Although there have been a significant number of studies on Rust security utilizing diverse techniques such as program analysis, fuzzing, privilege separation, and formal verification, existing studies suffer from three problems: 1) they only partially solve specific security issues but lack comprehensiveness; 2) most of them require manual interventions or annotations thus are not automated; and 3) they only cover a specific phase instead of the full lifecycle.In this perspective paper, we first survey current research progress on Rust security from 5 aspects, namely, empirical studies, vulnerability prevention, vulnerability detection, vulnerability rectification, and formal verification, and note the limitations of current studies. Then, we point out key challenges for Rust security. Finally, we offer our vision of a Rust security infrastructure guided by three principles: Comprehensiveness, Automation, and Lifecycle (CAL). Our work intends to promote the Rust security studies by proposing new research challenges and future research directions.

Rust is a new safe system programming language enforcing safety guarantees by novel language features, a rich type system, and strict compile-time checking rules, and thus has been used extensively to build system software. For multilingual Rust applications containing external C code, memory security vulnerabilities can occur due to the intrinsically unsafe nature of C and the improper interactions between Rust and C. Unfortunately, existing security studies on Rust only focus on pure Rust code but cannot analyze either the native C code or the Rust/C interactions in multilingual Rust applications. As a result, the lack of such studies may defeat the guarantee that Rust is a safe language.This paper presents CRust, a unified program analysis framework across Rust and C, which enables program analyses to understand the semantics of C code by translating Rust and C into a unified specification language. The CRust framework consists of three key components: (1) a unified specification language CRustIR, which is a strong-typed low-level intermediate language suitable for program analysis; (2) a transformation to build models of C code by converting C code into CRustIR; and (3) program analysis algorithms on CRustIR to detect security vulnerabilities. We have implemented a software prototype for CRust, and have conducted extensive experiments to evaluate its effectiveness and performance. Experimental results demonstrated that CRust can effectively detect common memory security vulnerabilities caused by the interaction of Rust and C that are missed by state-of-the-art tools. In addition, CRust is efficient in bringing negligible overhead (0.23 seconds on average).

Rust is an emerging programming language which aims to provide both safety guarantee and runtime efficiency, and has been used extensively in system programming scenarios. However, as Rust consists of an unsafe language subset unsafe, Rust programs are still vulnerable to severe security attacks which may defeat its safety guarantees. Existing studies on Rust security focus on the detection of vulnerabilities but seldom consider the bug fix issues. Meanwhile, it is often time-consuming and error-prone for Rust developers to understand and fix bugs manually, due to Rust’s advanced language features. In this paper, we present Rupair, an automated rectification system, to detect and fix one sort of the most severe Rust vulnerabilities—buffer overflows, and to help developers release secure Rust projects. The key technical component of Rupair is a novel security oriented lightweight data-flow analysis algorithm, which makes use of Rust’s two primary intermediate representations and works across the boundary of Rust’s safe and unsafe sub-languages. To evaluate the effectiveness of Rupair, we first apply it to all 4 reported buffer overflow-related CVEs and vulnerabilities (as of June 20, 2021). Experiment results demonstrated that Rupair successfully detected and rectified all these CVEs. To testify the scalability of Rupair, we collected 36 open-source Rust projects from 8 different application domains, consisting of 5,108,432 lines of Rust source code, and applied Rupair on these projects. Experiment results showed that Rupair successfully identified 14 previously undiscovered buffer overflow vulnerabilities in these projects, and rectified all of them. Moreover, Rupair is efficient, only introduced 3.6% overhead to each rectified Rust program on average.

Python has become one of the most popular pro-gramming languages in the era of data science and machine learning, and is also widely deployed in safety-critical fields like medical treatment, autonomous driving systems, etc. However, as the official and most widely used Python virtual machine, CPython, is implemented using C language, existing research has shown that the native code in CPython is highly vulnerable, thus defeats Python's guarantee of safety and security. This paper presents the design and implementation of PyGuard, a novel software prototype to find and understand real-world security vulnerabilities in the CPython virtual machines. With PyGuard, we carried out an empirical study of 10 different versions of CPython virtual machines (from version 3.0 to the latest 3.9). By scanning a total of 3,358,391 lines native code, we have identified 598 new vulnerabilities. Based on our study, we describe a taxonomy to classify vulnerabilities in CPython virtual machines. Our taxonomy provides a guidance to construct automated and accurate bug-finding tools. We also suggest systematic remedies that can mediate the threats posed by these vulnerabilities.

Safety is an important property of high-assurance software, and one of the hot research topics on it is the verification method for software to meet its safety policies. In our previous work, we designed a pointer logic system and proposed a framework for developing and verifying safety critical programs. And in this paper, we present the design and implementation of a certifying compiler based on that framework. Here we will mainly explain verification condition generation, generation of code and assertions, and proof generation for basic blocks. Our certifying compiler has the following novelties: 1) it supports a programming language equipped with both a type system and a logic system; 2) and it can produce safety proofs for programs with pointers.