-
ESBMC-Python: A Bounded Model Checker for Python Programs
Authors:
Bruno Farias,
Rafael Menezes,
Eddie B. de Lima Filho,
Youcheng Sun,
Lucas C. Cordeiro
Abstract:
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this…
▽ More
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
△ Less
Submitted 3 July, 2024;
originally announced July 2024.
-
Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking
Authors:
Janislley Oliveira de Sousa,
Bruno Carvalho de Farias,
Thales Araujo da Silva,
Eddie Batista de Lima Filho,
Lucas C. Cordeiro
Abstract:
Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an app…
▽ More
Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed.
△ Less
Submitted 9 November, 2023;
originally announced November 2023.
-
ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts
Authors:
Kunjian Song,
Nedas Matulevicius,
Eddie B. de Lima Filho,
Lucas C. Cordeiro
Abstract:
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which…
▽ More
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
△ Less
Submitted 25 November, 2021;
originally announced November 2021.
-
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
Authors:
Erickson H. da S. Alves,
Lucas C. Cordeiro,
Eddie B. de Lima Filho
Abstract:
Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threa…
▽ More
Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.
△ Less
Submitted 8 September, 2015;
originally announced September 2015.
-
Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)
Authors:
Felipe R. M. Sousa,
Lucas C. Cordeiro,
Eddie B. de Lima Filho
Abstract:
The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplifie…
▽ More
The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplified version of the Qt framework, which is integrated into the Efficient SMT-Based Bounded Model Checking tool to verify actual applications that use the mentioned framework. The method proposed in this paper presents a success rate of 94.45%, for the developed test suite.
△ Less
Submitted 5 September, 2015;
originally announced September 2015.
