Accuracy and rigor are vital indicators of the specification document, especially for the ARINC653 aviation industry standard. A high-quality standard or specification should clearly depict the system behaviors yet leave no fatal vulnerability. Formal verification could definitely help achieve this goal, but it requires intensive professional domain knowledge and overwhelming manpower. Recently, fast-growing natural language processing (NLP) techniques do well in harvesting knowledge extraction for the downstream tasks. However, since knowledge about an entity is scattered over heterogeneous contents (plain text, pseudocode, XML, etc.) for almost all such standard documents, a single content or not all contents cannot account for the entire knowledge. To this end, we propose a novel and practical approach to construct the Ontology of ARINC653 and extract the logical guards. Technically, we combine the NLP techniques with domainspecific naming and lexical rules for entity recognition in Ontology and then apply information extraction and relation formalization for relation extraction (in terms of guards). We evaluate the quality of our Ontology against that induced by the domain professor. We further apply this approach to the historical ARINC653 standards and evaluate the performance. Results show that our approach indeed helps construct knowledge integration and aid for specification understanding.

The rapid growth of the decentralized finance (DeFi) ecosystem has given rise to flash loan, a type of uncollateralized loan service that enables users to easily borrow substantial amounts of funds. However, this has prompted attackers to conduct malicious arbitrage within DeFi protocols, known as notorious flash loan attacks, resulting in significant asset losses. Existing works primarily focus on investigating price oracle manipulation, a common tactic in flash loan attacks, but lack a comprehensive understanding regarding the entire process of flash loan attacks and the diverse range of attack methods. In this paper, we empirically study 155 real-world flash loan attack incidents, representing the largest-scale study to date. We first categorize these incidents into five types based on their root causes and compile statistics on their distribution, then elucidate the vulnerable code and finance mechanisms exploited in each category. Subsequently, we identify the symptoms of codebased vulnerabilities and summarize the abstract attack models for the entire process. Finally, we evaluate the effectiveness of state-of-the-art off-chain tools in detecting code-based vulnerabilities within their scope of capabilities. We find that Slither performs the best in detecting 22 % of temporal reentrancy vulnerabilities, and DeFiTainter has a 52% false negative rate in detecting price oracle manipulation, mainly attributed to three limitations.

As a relatively new programming language, Rust is designed to provide both memory safety and runtime performance. To achieve this goal, Rust conducts rigorous static checks against its safety rules during compilation, effectively eliminating memory safety issues that plague C/C++ programs. Although useful, the safety rules pose programming challenges to Rust programmers, since programmers can easily violate safety rules when coding in Rust, leading their code to be rejected by the Rust compiler, a fact underscored by a recent user study. There exists a desire to automate the process of fixing safety-rule violations to enhance Rust's programmability.

Rust is a relatively new programming language known for its memory safety and numerous advanced features. It has been widely used in system software in recent years. Thus, ensuring the reliability and robustness of the only implementation of the Rust compiler, rustc, is critical. However, compiler testing, as one of the most effective techniques to detect bugs, faces difficulties in generating valid Rust programs with sufficient diversity due to its stringent memory safety mechanisms. Furthermore, existing research primarily focuses on testing rustc to trigger crash errors, neglecting incorrect compilation results - miscompilation. Detecting miscompilation remains a challenge in the absence of multiple implementations of the Rust compiler to serve as a test oracle.

Smart contracts are becoming appealing targets for hackers because of the vast amount of cryptocurrencies under their control. Asset loss due to the exploitation of smart contract codes has increased significantly in recent years. To guarantee that smart contracts are vulnerability-free, there are many works to detect the vulnerabilities of smart contracts, but only a few vulnerability repair works have been proposed. Repairing smart contract vulnerabilities at the source code level is attractive as it is transparent to users, whereas existing repair tools, such as SCRepair and sGuard , suffer from many limitations: (1) ignoring the code of vulnerability prevention; (2) possibly applying the repair to the wrong statements and changing the original business logic of smart contracts; and (3) showing poor performance in terms of time and gas overhead. In this work, we propose machine learning guided rule-based automated vulnerability repair on smart contracts to improve the effectiveness and efficiency of sGuard . To address the limitations mentioned above, we design the features that characterize both the symptoms of vulnerabilities and the methods of vulnerability prevention to learn various vulnerability patterns and reduce false positives. Additionally, a fine-grained localization algorithm is designed by traversing the nodes of the abstract syntax tree, and we refine and extend the repair rules of sGuard to preserve the original business logic of smart contracts and support new vulnerability types. Our tool, named sGuard+ , reduces time overhead based on machine learning models, and reduces gas overhead by fewer code changes and precise patching. In our experiment, we collect a publicly available vulnerability dataset from CVE, SWC, and SmartBugs Curated as a ground truth for evaluations. Overall, sGuard+ repairs more vulnerabilities with less time and gas overhead than state-of-the-art tools. Furthermore, we reproduce about 9,000 historical transactions for regression testing. It is shown that sGuard+ has no impact on the original business logic of smart contracts.