scholarly journals Symbiotic 8: Beyond Symbolic Execution

2021 ◽  
pp. 453-457
Author(s):  
Marek Chalupa ◽  
Tomáš Jašek ◽  
Jakub Novák ◽  
Anna Řechtáčková ◽  
Veronika Šoková ◽  
...  
Keyword(s):  
Shape Analysis ◽  
Symbolic Execution ◽  
Program Slicing ◽  
Analysis Tool ◽  
Light Weight ◽  
Weight Analysis ◽  
Correctness Of Programs

AbstractSymbiotic 8 extends the traditional combination of static analyses, instrumentation, program slicing, and symbolic execution with one substantial novelty, namely a technique mixing symbolic execution with k-induction. This technique can prove the correctness of programs with possibly unbounded loops, which cannot be done by classic symbolic execution.Symbiotic 8 delivers also several other improvements. In particular, we have modified our fork of the symbolic executorKleeto support the comparison of symbolic pointers. Further, we have tuned the shape analysis toolPredator(integrated already inSymbiotic 7) to perform better onllvmbitcode. We have also developed a light-weight analysis of relations between variables that can prove the absence of out-of-bound accesses to arrays.

Predator Shape Analysis Tool Suite

2016 ◽  
pp. 202-209 ◽  
Author(s):  
Lukáš Holík ◽  
Michal Kotoun ◽  
Petr Peringer ◽  
Veronika Šoková ◽  
Marek Trtík ◽  
...  
Keyword(s):  
Shape Analysis ◽  
Analysis Tool

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.

scholarly journals Symbolic Execution Based Intra-Procedural Analysis for Search for Defects

2020 ◽  
Vol 32 (6) ◽  
pp. 87-100
Author(s):  
Alexey Evgenevich Borodin ◽  
Irina Aleksandrovna Dudina
Keyword(s):  
Symbolic Execution ◽  
Analysis Tool ◽  
Bug Detection ◽  
Call Graph ◽  
Quality Of Reports ◽  
Speed Up ◽  
Abstract Domains ◽  
Value Numbering ◽  
Static Analysis Tool

Svace is a static analysis tool for bug detection in C/C++/Java source code. To analyze a program, Svace performs an intra-procedure analysis of individual functions, starting from the leaves of a call-graph and moving towards the roots, and uses summaries of previously analyzed procedures at call-cites. In this paper, we overview the approaches and techniques employed by Svace for the intra-procedural analysis. This phase is performed by an analyzer engine and an extensible set of detectors. The core engine employs a symbolic execution approach with state merging. It uses value numbering to reduce the set of symbolic expressions, maintains points-to relationship graph for memory modeling, and performs strong and weak updates of program values. Detectors are responsible for discovering and reporting bugs. They calculate different properties of program values using a variety of abstract domains. All detectors work simultaneously orchestrated by the engine. Svace analysis is unsound and employs a variety of heuristics to speed-up. We designed Svace to analyze big projects (several MLOCs) in just a few hours and report as many warnings as possible, while keeping a good quality of reports ≥ 65 of true positives). For example, Tizen 5.5 (20MLOC) analysis takes 8.6 hours and produces 18,920 warnings, more than 70% of which are true-positive.

Pattern shape analysis tool for defect judgement of photomask

2000 ◽  
Author(s):  
Fuyuhiko Matsuo ◽  
Masao Otaki ◽  
Norihito Fukugami ◽  
Isao Yonekura ◽  
Yuhichi Fukushima
Keyword(s):  
Shape Analysis ◽  
Analysis Tool ◽  
Pattern Shape

scholarly journals Searching for tainted vulnerabilities in static analysis tool Svace

2021 ◽  
Vol 33 (1) ◽  
pp. 7-32
Author(s):  
Alexey Evgenevich Borodin ◽  
Alexey Vyacheslavovich Goremykin ◽  
Sergey Pavlovitch Vartanov ◽  
Andrey Andreevich Belevantsev
Keyword(s):  
High Speed ◽  
Symbolic Execution ◽  
False Negative ◽  
False Negative Rate ◽  
False Positives ◽  
Analysis Tool ◽  
Main Function ◽  
Smt Solver ◽  
Call Graph ◽  
Low Level

The paper is dedicated to search for taint-based errors in the source code of programs, i.e. errors caused by unsafe use of data obtained from external sources, which could potentially be modified by an attacker. The interprocedural static analyzer Svace was used as a basis. The analyzer searches both for defects in the program and searches for suspicious places where the logic of the program may be violated. The goal is to find as many errors as possible at an acceptable speed and a low level of false positives (< 20-35%). To find errors, Svace with help of modified compiler builds a low-level typed intermediate representation, which is used as an input to the main SvEng analyzer. The analyzer builds a call graph and then performs summary-based analysis. In this analysis, the functions are traversed according to the call graph starting from the leaves. After analyzing the function, its summary is created, which will then be used to analyze the call instructions. The analysis has both high speed and good scalability. Intra-procedural analysis is based on symbolic execution with the union of states at merge points of paths. An SMT solver can be used to filter out infeasible paths for some checkers. In this case, the SMT-solver is called only if there is a suspicion of an error. The analyzer has been expanded to find defects of tainted data using. The checkers are implemented as plugins by using the source-sink scheme. The sources are calls of library functions that receive data from outside the program, as well as the arguments of the main function. Sinks are accessing to arrays, using variables as a step or loop boundary, calling functions that require checked arguments. Checkers covering most of the possible types of vulnerabilities for tainted integers and strings have been implemented. The Juliet project was used to assess the coverage. The false negative rate ranged from 46,31% to 81.17% with a small number of false positives.

scholarly journals An efficient numerical shape analysis for light weight membrane structures

2014 ◽  
Vol 15 (4) ◽  
pp. 255-271 ◽  
Author(s):  
Chao Yang ◽  
Yan-bin Shen ◽  
Yao-zhi Luo
Keyword(s):  
Shape Analysis ◽  
Light Weight ◽  
Membrane Structures

Pattern shape analysis tool for quantitative estimate of photomask and process

2001 ◽  
Author(s):  
Isao Yonekura ◽  
Yuhichi Fukushima ◽  
Fuyuhiko Matsuo ◽  
Masao Otaki ◽  
Norihito Fukugami
Keyword(s):  
Shape Analysis ◽  
Quantitative Estimate ◽  
Analysis Tool ◽  
Pattern Shape

scholarly journals Quantitative analysis for symbolic heap bounds of CPS software

2011 ◽  
Vol 8 (4) ◽  
pp. 1251-1276 ◽  
Author(s):  
Renjian Li ◽  
Ji Wang ◽  
Liqian Chen ◽  
Wanwei Liu ◽  
Dengping Wei
Keyword(s):  
Shape Analysis ◽  
Symbolic Execution ◽  
Analysis Method ◽  
Physical Systems ◽  
State Transition Graph ◽  
Systems Software ◽  
Quantitative Property ◽  
Precise Analysis ◽  
Numeric Representation ◽  
Numeric Reasoning

One important quantitative property of CPS (Cyber-Physical Systems) software is its heap bound for which a precise analysis result needs to combine shape analysis and numeric reasoning. In this paper, we present a framework for statically finding symbolic heap bounds of CPS software. The basic idea is to separate numeric reasoning from shape analysis by first constructing an ASTG (Abstract State Transition Graph) and then extracting a pure numeric representation which can be analyzed for the heap bounds. A quantitative shape analysis method based on symbolic execution is defined in the framework to generate the ASTG. The numeric representation is extracted based on program slicing technique and inputted into an abstract interpretation tool for computing the heap bounds. We take list manipulating programs as an example to explain how to instantiate the framework for important data structures and to exhibit its practicability. A novel list abstraction method is also presented to support the instantiation of the framework.

scholarly journals Railway Software Analysis Tool using Symbolic Execution Method

2016 ◽  
Vol 65 (4) ◽  
pp. 242-249
Author(s):  
Hyun-Jeong Jo ◽  
Jong-Gyu Hwang ◽  
Duck-Ho Shin
Keyword(s):  
Symbolic Execution ◽  
Analysis Tool ◽  
Software Analysis
Sign in / Sign up

Export Citation Format

Share Document