scholarly journals Map2Check: Using Symbolic Execution and Fuzzing

2020 ◽  
pp. 403-407 ◽  
Author(s):  
Herbert Rocha ◽  
Rafael Menezes ◽  
Lucas C. Cordeiro ◽  
Raimundo Barreto
Keyword(s):  
Software Verification ◽  
Symbolic Execution ◽  
Source Code ◽  
Reachability Analysis ◽  
Experimental Results ◽  
Safety Properties ◽  
C Programs ◽  
Verification Tool ◽  
Inductive Invariants ◽  
Monitor Data

Abstract Map2Check is a software verification tool that combines fuzzing, symbolic execution, and inductive invariants. It automatically checks safety properties in C programs by adopting source code instrumentation to monitor data (e.g., memory pointers) from the program’s executions using LLVM compiler infrastructure. For SV-COMP 2020, we extended Map2Check to exploit an iterative deepening approach using LibFuzzer and Klee to check for safety properties. We also use Crab-LLVM to infer program invariants based on reachability analysis. Experimental results show that Map2Check can handle a wide variety of safety properties in several intricate verification tasks from SV-COMP 2020.

scholarly journals Improved Loop Execution Modeling in the Clang Static Analyzer

2020 ◽  
Author(s):  
Péter György Szécsi ◽  
Gábor Horváth ◽  
Zoltán Porkoláb
Keyword(s):  
Arbitrary Number ◽  
Symbolic Execution ◽  
Source Code ◽  
Current Method ◽  
Analysis Tool ◽  
Constant Number ◽  
Loop Modeling ◽  
Code Analysis ◽  
C Programs ◽  
Alternative Approaches

The LLVM Clang Static Analyzer is a source code analysis tool which aims to find bugs in C, C++, and Objective-C programs using symbolic execution, i.e. it simulates the possible execution paths of the code. Currently the simulation of the loops is somewhat naive (but efficient), unrolling the loops a predefined constant number of times. However, this approach can result in a loss of coverage in various cases. This study aims to introduce two alternative approaches which can extend the current method and can be applied simultaneously: (1) determining loops worth to fully unroll with applied heuristics, and (2) using a widening mechanism to simulate an arbitrary number of iteration steps. These methods were evaluated on numerous open source projects, and proved to increase coverage in most of the cases. This work also laid the infrastructure for future loop modeling improvements.

Concurrent Bug Finding Based on Bounded Model Checking

2020 ◽  
Vol 30 (05) ◽  
pp. 669-694
Author(s):  
Milena Vujošević Janičić
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Sequential Approach ◽  
Software Analysis ◽  
Verification Tool ◽  
Single Compound ◽  
Bug Finding ◽  
Reliable Software

Automated and reliable software verification is of crucial importance for development of high-quality software. Formal methods can be used for finding different kinds of bugs without executing the software, for example, for finding possible run-time errors. The methods like model checking and symbolic execution offer very precise static analysis but on real world programs do not always scale well. One way to tackle the scalability problem is to apply new concurrent and sequential approaches to complex algorithms used in these kinds of software analysis. In this paper, we compare different variants of bounded model checking and propose two concurrent approaches: concurrency of intra-procedural analysis and concurrency of inter-procedural analysis. We implemented these approaches in a software verification tool LAV, a tool that is based on bounded model checking and symbolic execution. For assessing the improvements gained, we experimentally compared the concurrent approaches with the standard bounded model checking approach (where all correctness conditions are put into a single compound formula) and with a sequential approach (where correctness conditions are checked separately, one after the other). The results show that, in many cases, the proposed concurrent approaches give significant improvements.

scholarly journals Verification and refutation of C programs based on k-induction and invariant inference

2020 ◽  
Author(s):  
Omar M. Alhawi ◽  
Herbert Rocha ◽  
Mikhail R. Gadelha ◽  
Lucas C. Cordeiro ◽  
Eddie Batista
Keyword(s):  
Embedded System ◽  
Control Systems ◽  
Software Verification ◽  
Bounded Model Checking ◽  
Safety Properties ◽  
C Programs ◽  
Software Applications ◽  
Verification Algorithm ◽  
Source Transformation ◽  
Proof By Induction

Abstract DepthK is a source-to-source transformation tool that employs bounded model checking (BMC) to verify and falsify safety properties in single- and multi-threaded C programs, without manual annotation of loop invariants. Here, we describe and evaluate a proof-by-induction algorithm that combines k-induction with invariant inference to prove and refute safety properties. We apply two invariant generators to produce program invariants and feed these into a k-induction-based verification algorithm implemented in DepthK, which uses the efficient SMT-based context-bounded model checker (ESBMC) as sequential verification back-end. A set of C benchmarks from the International Competition on Software Verification (SV-COMP) and embedded-system applications extracted from the available literature are used to evaluate the effectiveness of the proposed approach. Experimental results show that k-induction with invariants can handle a wide variety of safety properties, in typical programs with loops and embedded software applications from the telecommunications, control systems, and medical domains. The results of our comparative evaluation extend the knowledge about approaches that rely on both BMC and k-induction for software verification, in the following ways. (1) The proposed method outperforms the existing implementations that use k-induction with an interval-invariant generator (e.g., 2LS and ESBMC), in the category ConcurrencySafety, and overcame, in others categories, such as SoftwareSystems, other software verifiers that use plain BMC (e.g., CBMC). Also, (2) it is more precise than other verifiers based on the property-directed reachability (PDR) algorithm (i.e., SeaHorn, Vvt and CPAchecker-CTIGAR). This way, our methodology demonstrated improvement over existing BMC and k-induction-based approaches.

Synthesizing Conjunctive & Disjunctive Linear Invariants by K-means++ and SVM

2020 ◽  
Vol 17 (6) ◽  
pp. 847-856
Author(s):  
Shengbing Ren ◽  
Xiang Zhang
Keyword(s):  
Software Verification ◽  
State Of The Art ◽  
Positive Sample ◽  
Machine Learning Algorithms ◽  
Support Vector ◽  
Hoare Logic ◽  
Excellent Performance ◽  
Automated Software ◽  
Inductive Invariants ◽  
Linear Invariants

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

scholarly journals ATLaS: Assistant Software for Life Scientists to Use in Calculations of Buffer Solutions

2021 ◽  
Vol 15 (4) ◽  
pp. 541-545
Author(s):  
Ugur Comlekcioglu ◽  
Nazan Comlekcioglu
Keyword(s):  
Programming Language ◽  
Life Science ◽  
Source Code ◽  
Experimental Results ◽  
Acid Base ◽  
Buffer Solutions ◽  
Python Programming Language ◽  
Science Laboratories ◽  
Executable File ◽  
Python Programming

Many solutions such as percentage, molar and buffer solutions are used in all experiments conducted in life science laboratories. Although the preparation of the solutions is not difficult, miscalculations that can be made during intensive laboratory work negatively affect the experimental results. In order for the experiments to work correctly, the solutions must be prepared completely correctly. In this project, a software, ATLaS (Assistant Toolkit for Laboratory Solutions), has been developed to eliminate solution errors arising from calculations. Python programming language was used in the development of ATLaS. Tkinter and Pandas libraries were used in the program. ATLaS contains five main modules (1) Percent Solutions, (2) Molar Solutions, (3) Acid-Base Solutions, (4) Buffer Solutions and (5) Unit Converter. Main modules have sub-functions within themselves. With PyInstaller, the software was converted into a stand-alone executable file. The source code of ATLaS is available at https://github.com/cugur1978/ATLaS.

scholarly journals FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)

2021 ◽  
pp. 363-367 ◽  
Author(s):  
Kaled M. Alshmrany ◽  
Rafael S. Menezes ◽  
Mikhail R. Gadelha ◽  
Lucas C. Cordeiro
Keyword(s):  
Model Checking ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Test Cases ◽  
Security Vulnerabilities ◽  
C Programs ◽  
Code Coverage

AbstractWe describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. successfully participates in Test-Comp’21 and achieves first place in the category and second place in the category.

scholarly journals Reachability Modulo Theory Library

10.29007/f3rp ◽  
2018 ◽  
Author(s):  
Francesco Alberti ◽  
Roberto Bruttomesso ◽  
Silvio Ghilardi ◽  
Silvio Ranise ◽  
Natasha Sharygina
Keyword(s):  
Reachability Analysis ◽  
Safety Properties ◽  
Standard Language ◽  
Transition Systems ◽  
Smt Solvers ◽  
Verification Tools ◽  
Infinite State Systems ◽  
Infinite State

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

Concolic Test Generation and the Cloud

2015 ◽  
pp. 302-322
Author(s):  
Nikolai Kosmatov
Keyword(s):  
Software Testing ◽  
Test Generation ◽  
Symbolic Execution ◽  
Major Obstacle ◽  
Testing Methods ◽  
C Programs ◽  
Security Issues ◽  
Efficient Alternative ◽  
Cloud Environments ◽  
Testing Techniques

Software testing in the cloud can reduce the need for hardware and software resources and offer a flexible and efficient alternative to the traditional software testing process. A major obstacle to the wider use of testing in the cloud is related to security issues. This chapter focuses on test generation techniques that combine concrete and symbolic execution of the program under test. Their deployment in the cloud leads to complex technical and security issues that do not occur for other testing methods. This chapter describes recent online deployment of such a technique implemented by the PathCrawler test generation tool for C programs, where the author faced, studied, and solved many of these issues. Mixed concrete/symbolic testing techniques not only constitute a challenging target for deployment in the cloud, but they also provide a promising way to improve the reliability of cloud environments. The author argues that these techniques can be efficiently used to help to create trustworthy cloud environments.

A Virtual Laboratory for Digital Signal Processing

2008 ◽  
pp. 474-487
Author(s):  
Chyi-Ren Dow ◽  
Yi-Hsung Li ◽  
Jin-Yu Bai
Keyword(s):  
Signal Processing ◽  
Digital Signal Processing ◽  
Mobile Agent ◽  
Source Code ◽  
Digital Signal ◽  
Experimental Results ◽  
Positive Feedbacks ◽  
Network Bandwidth ◽  
Network Capability ◽  
Java Native Interface

This work designs and implements a virtual digital signal processing laboratory, VDSPL. VDSPL consists of four parts: mobile agent execution environments, mobile agents, DSP development software, and DSP experimental platforms. The network capability of VDSPL is created by using mobile agent and wrapper techniques without modifying the source code of the original programs. VDSPL provides human-human and human-computer interaction for students and teachers, and it can also lighten the loading of teachers, increase the learning result of students, and improve the usage of network bandwidth. A prototype of VDSPL has been implemented by using the IBM Aglet system and Java Native Interface for DSP experimental platforms. Also, experimental results demonstrate that our system has received many positive feedbacks from both students and teachers.

Sign in / Sign up

Export Citation Format

Share Document