hbgit / map2check Goto Github PK
View Code? Open in Web Editor NEWMap2Check: Finding Software Vulnerabilities
Home Page: https://map2check.github.io
License: GNU General Public License v2.0
Map2Check: Finding Software Vulnerabilities
Home Page: https://map2check.github.io
License: GNU General Public License v2.0
Bug in reachability analysis
Verification tasks in SV-COMP
../../sv-benchmarks/c/bitvector/byte_add-2.i
Fix check for shift operation r3 << 24U, see ISO/IEC 9899:2011 6.5.7#4, in that case r3<<24U will exceed INT_MAX
../../sv-benchmarks/c/bitvector/byte_add_1-2.i
Not identified bug root, but we have modeling issues with shift operation
../../sv-benchmarks/c/bitvector/byte_add_2-1.i
Not identified bug root, but we have modeling issues with shift operation
Verification results from SV-COMP
../../sv-benchmarks/c/ldv-regression/sizeofparameters_test.i
Incorrect long int a = __VERIFIER_nondet_long(); representation
../../sv-benchmarks/c/ldv-regression/test27-2.c
Expected FALSE, but the result is TRUE
Check:
libfuzzer -> ERROR: UndefinedBehaviorSanitizer: SEGV on unknown address
KLEE -> memory error: out of bound pointer
OR -> Struct modeling error
../../sv-benchmarks/c/ldv-regression/test28-1.c
>> Same ERROR as the ldv-regression/test27-2.c
Add CII Best Practices Badge Program
Check out the info at https://bestpractices.coreinfrastructure.org
More information on the CII Best Practices Badging program, including background and criteria, is available on GitHub. Project statistics and criteria statistics are available.
Adopt a code slicer
Aiming to improve the code exploration and avoiding states in the program unnecessary to prove a given property, you could adopt a code slicer.
Checking out some slicers:
Aiming to improve Map2Check to handle different types of licenses. I would like to suggest to add SPDX-License-Identifier. Check out https://spdx.org/ids
I would like to suggest you update KLEE and uClibc, check out:
KLEE: https://github.com/klee/klee/releases/tag/v2.1
uClibc: https://github.com/klee/klee-uclibc/tree/klee_uclibc_v1.2
New subcategories from SV-COMP not supported yet
Apply minor changes to support:
We should use the Clang/LLVM API instead of calling external binaries. For example, the older version used this
Places where refactoring is needed:
Also, some other fixes for caller (we should open an issue for Caller class only):
Originally posted by @RafaelSa94 in #8 (comment)
Is your feature request related to a problem? Please describe.
Currently, we only have support for KLEE as a symbolic engine, the issue is that it contains a limitation for floating numbers. Crucible supports enconding for floats
, has support for SV-COMP notation and it's API contains all that is needed for a Generator.
Describe the solution you'd like
Implement a NonDetGeneratorCrucible
and compare it with KLEE specially for floats.
Verification tasks from SV-COMP
Expected FALSE, but result is TRUE
Incorrect mapping = BUG
LOC 16, not checked ptr scope
Incorrect mapping = ptr not initialized
Incorrect mapping = incorrect initialized
pthread not modelling, I suggest you to create a new issue
Incorrect modelling struct and void
Is your feature request related to a problem? Please describe.
Not related to a problem. Currently, we default to -O3 optimizations and let KLEE decides which solver to be used. The -O3 may not be the best for Symbolic Execution and the SMT formula generated by KLEE may not be the best for the selected solver.
Describe the solution you'd like
We should select which solver and the best optimization for Symbolic Execution.
Describe alternatives you've considered
Extend Map2Check to have a class to select which optimizations will be done.
Additional context
The paper Studying the influence of standard compiler optimizations on symbolic execution contains details on how LLVM optimizations affects KLEE and the solvers
Is your feature request related to a problem? Please describe.
FuseBMC is trying to use map2check to create coverage for C programs. However, its targets consists in functions named GOAL_N (where N is a number).
Describe the solution you'd like
Add the option --target-function-name
which will set the target function name for map2check. This will require patches over the TargetPass and over the opt calls.
Describe alternatives you've considered
The tool that is using map2check could instead rename the current target into __VERIFIER_error()
Additional context
Some reference:
In the current experiments, KLEE adopt only one core from CPU. I propose to adopt the following solution:
This is mainly because when we try to check program correctness.
Checkout the following branches, aiming to update or remove from the project:
KLEE-Float
Check out https://srg.doc.ic.ac.uk/projects/klee-float/
That is an extension project to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic. For more details see:
Floating-Point Symbolic Execution: A Case Study in N-version Programming. Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair Donaldson, Rafael Zähl, Klaus Wehrle. IEEE/ACM International Conference on Automated Software Engineering (ASE 2017)
Checkout https://smt-comp.github.io/2019/results
Is it possible to run different smt solver in parallel?
Is it possible to update the default smt solver?
Try Yices 2.6.2 (http://yices.csl.sri.com/) or Boolector (https://boolector.github.io/)
Change code on:
https://github.com/hbgit/Map2Check/blob/develop/modules/frontend/map2check.cpp#L153
https://github.com/hbgit/Map2Check/blob/develop/modules/frontend/map2check.cpp#L208
https://github.com/hbgit/Map2Check/blob/develop/modules/frontend/caller.cpp#L309
Check out this sample: https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c
I would suggest to you add a checker result when CrabLLVM was adopted in the verification.
Verification tasks from SV-COMP
One possible solution for the incorrect true results is to adopt a redundant check.
Add program invariant result in ERROR
libfuzzer out: fuzzing was not performed, you have only executed the target code on a fixed set of inputs.
../../sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c
- Checking KLEE options
- Bug in process KLEE result "KLEE: WARNING: error opening file"
../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
- Bug in process KLEE result "KLEE: WARNING: error opening file"
../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
- Bug in process KLEE result "KLEE: WARNING: error opening file"
KLEE was not able to find the bug:
Fix incorrect call of CRABLLVM
I would like to suggest you skip the CRABLLVM call to run fuzzing.
Start at:
Update to LLVM 8.0
Aiming to reduce the docker image and apply new futures from LLVM 8
Verification tasks from SV-COMP
You need to improve memory leak check, bug root new_head->data_2 = __VERIFIER_nondet_int() == len? 1 : 0;
expected_verdict: false but the result is TRUE
Add support for new reach function
Checking out sosy-lab/sv-benchmarks@28369c9
Check KLEE output after the map2check verification
KLEE crashes and incorrect TRUE results for Map2Check mode (e.g., target generate prt error).
I would like to suggest you check out the KLEE output before to show TRUE answer for the verification task.
Is your feature request related to a problem? Please describe.
I'd like to run only KLEE or only libFuzzer (or any future generator)
Describe the solution you'd like
Add the --generator option with klee and libfuzerr as valid values
Describe alternatives you've considered
None
Additional context
It should be simple, the major change will be at the wrapper of the interaction between klee and libFuzzer will have to be refactored.
Termination Analysis
Add support to verify the category Termination-MainControlFlow on SV-COMP that contains programs for which termination should be decided.
I suggest you check out the follows paper:
Also suggest you to check SeaHorn tool.
Add support for concurrency programs, e.g., the category ConcurrencySafety.
One possible solution is to adopt Lazy-Cseq* (https://www.southampton.ac.uk/~gp1y10/cseq/) tool to generate the C code, then apply Map2Check tool with its features to improve de verification. Note that Lazy-Cseq generates nondet calls for KLEE.
*CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization.
Inferring program invariant adopting templates
Adopting InvGen flow
Skipping to call nondet generator
I would like to suggest to avoid call fuzzer or symbolic execution when a program does not have a nondet function.
Verification tasks from SV-COMP
../../sv-benchmarks/c/signedintegeroverflow-regression/AdditionIntMax.i
It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
the sum result (2147483647 + 1) is not allowed in int type of sizeof(int) = 4
../../sv-benchmarks/c/signedintegeroverflow-regression/Multiplication-2.i
It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
the mult result (65536 * 32768) is not allowed in int type of sizeof(int) = 4
../../sv-benchmarks/c/signedintegeroverflow-regression/NoConversion.i
It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
the sum result long x = 2147483647 + 1; is not allowed in long type of sizeof(long or long int) = 4
Could you adopt https://coveralls.io/repos
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.