KLEE Symbolic Execution Engine

KLEE Symbolic Virtual Machine

Build Status Build Status Build Status Coverage

KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components:

  1. The core symbolic virtual machine engine; this is responsible for executing LLVM bitcode modules with support for symbolic values. This is comprised of the code in lib/.

  2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with additional support for making parts of the operating system environment symbolic.

Additionally, there is a simple library for replaying computed inputs on native code (for closed programs). There is also a more complicated infrastructure for replaying the inputs generated for the POSIX/Linux emulation layer, which handles running native programs in an environment that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments.

For further information, see the webpage.

Owner
KLEE
The KLEE Dynamic Symbolic Execution Engine and related projects
KLEE
Comments
  • Add support for exception handling (C++ 6/6)

    Add support for exception handling (C++ 6/6)

    This PR is part of a chain of PRs that adds C++-support to KLEE. This is the final (and 'main') PR of the chain, the other PRs are:

    • [x] ~~#961 - Adds basic support for memalign~~ (dropped; see the PR for infos; new PR: #988)
    • [x] ~~#962 - Adds support for newlocale and freelocale (e.g., required for cout).~~ (will be done in uclibc; see the PR for infos)
    • [x] #963 - ~~Implements some~~ Enables lowering of atomic LLVM instructions.
    • [x] #964 - Adds a hack to support landingpad instructions.
    • [x] ~~#965 - Adds capabilities to KLEE and KLEE's build system to allow linking against a libcxx.~~ Implemented in #1056.
    • [ ] This PR (#966) - Adds support for exception handling.

    These PRs form a chain, therefore they need to be merged from the top (e.g., top one first, while this PR can only be merged last). If required, there is some room to change the merge order, but some hard dependencies exist.

    The main PRs are the two last ones, those which add support for building against a libcxx and support for exception handling. However, while the others are smaller, they are still required in order to analyze programs built and linked against a libcxx and using exceptions.


    This PR adds support for exception handling and unwinding to KLEE, also supporting nested exceptions. The new tests show the added capabilities.

    This is implemented by keeping track of a current stack of exception frames per state once unwinding begins, i.e., __cxa_throw is called. When unwinding is invoked in LLVM, control flow will transfer to the next landingpad block in the current call chain. A landingpad can be specified in LLVM by using invoke instead of call, which takes the target landingpad - where control flow should resume in case of an exception - as an extra argument. Different eh_typeids can be used to continue control flow at different blocks depending on the type of the exception that is being thrown (e.g., when using different catch-blocks in C++).

    When a new exception is thrown, KLEE keeps track of the bottom and top stack frame indices of this exception. If execution unwinds below the bottomStackFrameIndex, it is uncaught, and an error is raised. The topStackFrameIndex adds support for nested exceptions, e.g., when a new exception is thrown inside a catch-block. As long as this new exception is caught inside this catch-block, it is not an error. Therefore, nested catch-blocks need to be supported, as well as nested try-blocks. See the tests nested.cpp and nested_fail.cpp for examples of this.

    This PR also adds tests for a lot more general C++ functionality.

  • Implement basic support for vectorized instructions.

    Implement basic support for vectorized instructions.

    We use LLVM's Scalarizer pass to remove most vectorized code so that the Executor only needs to support the InsertElement and ExtractElement instructions.

    This pass was not available in LLVM 3.4 so to support that LLVM version the pass has been back ported.

    There is no support for LLVM 2.9.

    There are a few limitations to this implementation.

    • The InsertElement and ExtractElement index cannot be symbolic.
    • Due to the lack of proper floating point support the float_vector_constant_llvm*.ll tests currently do not pass.
  • IndependentSolver bug

    IndependentSolver bug

    Hi all, I am running some experiments with KLEE on Coreutils 6.11 and I deterministically experience this crash on date and touch utility:

    KLEE: HaltTimer invoked  
    KLEE: halting execution, dumping remaining states  
    klee: IndependentSolver.cpp:532: virtual bool IndependentSolver::computeInitialValues(const klee::Query&, const std::vector<const klee::Array*>&, std::vector<std::vector<unsigned char> >&, bool&): Assertion `assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"' failed.  
    0  libLLVM-3.4.so.1 0x00007fca47c60d62 llvm::sys::PrintStackTrace(_IO_FILE*) + 50  
    1  libLLVM-3.4.so.1 0x00007fca47c607bc  
    2  libpthread.so.0  0x00007fca46cb8d10  
    3  libc.so.6        0x00007fca45e41267 gsignal + 55  
    4  libc.so.6        0x00007fca45e42eca abort + 362  
    5  libc.so.6        0x00007fca45e3a03d  
    6  libc.so.6        0x00007fca45e3a0f2  
    7  klee             0x00000000004f24ac IndependentSolver::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 8012  
    8  klee             0x00000000004f8aa9 QueryLoggingSolver::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 73  
    9  klee             0x00000000004fd4b3 klee::Solver::getInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&) + 35  
    10 klee             0x00000000004b8d57 klee::TimingSolver::getInitialValues(klee::ExecutionState const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&) + 263  
    11 klee             0x000000000048899b klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 763  
    12 klee             0x0000000000480e4e KleeHandler::processTestCase(klee::ExecutionState const&, char const*, char const*) + 302  
    13 klee             0x000000000048930a klee::Executor::terminateStateEarly(klee::ExecutionState&, llvm::Twine const&) + 394  
    14 klee             0x00000000004989d1 klee::Executor::run(klee::ExecutionState&) + 1377  
    15 klee             0x000000000049937c klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1644  
    16 klee             0x0000000000476c2e main + 11326  
    17 libc.so.6        0x00007fca45e2ca40 __libc_start_main + 240  
    18 klee             0x000000000047e0f9 _start + 41  
    Aborted (core dumped)  
    

    My setup: Ubuntu 15.10 LLVM 3.4 KLEE (built with uclibc) 2a0eca5 STP 3785148da15919de445e476a6f20b06c881cf50c Coreutils 6.11 built with whole-program-llvm (with clang as llvm compiler) and configured as in the KLEE tutorial page

    I experience this bug also in this setup: Ubuntu 15.10 LLVM 2.9 KLEE (built with uclibc) 2a0eca5 STP 3785148da15919de445e476a6f20b06c881cf50c Coreutils 6.11 built with klee-gcc and configured as in the KLEE tutorial page

    The commands I use: klee --libc=uclibc --posix-runtime -use-query-log=all:pc --simplify-sym-indices --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 --use-cex-cache=false ../coreutils-6.11/obj-llvm/src/date.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

    klee --libc=uclibc --posix-runtime -use-query-log=all:pc --simplify-sym-indices --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. --max-memory-inhibit=false --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 --use-cex-cache=false ../coreutils-6.11/obj-llvm/src/touch.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

    The counterexample cache is disabled as per issue #347. The assertion fails both with and without -optimize option. Moreover, the assertion fails deterministically not only in KLEE but also in KLEAVER for example with the following query:

    array n_args[4] : w32 -> w8 = symbolic                                                                                                                                                                                                                                          
    array n_args_1[4] : w32 -> w8 = symbolic                                                                                                                                                                                                                                        
    array A-data-stat[144] : w32 -> w8 = symbolic                                                                                                                                                                                                                                   
    array stdin-stat[144] : w32 -> w8 = symbolic                                                                                                                                                                                                                                    
    (query [(Ult N0:(ReadLSB w32 0 n_args) 2)                                                                                                                                                                                                                                                                
    (Slt 0 N0)
    (Ult N1:(ReadLSB w32 0 n_args_1) 3)
    (Slt 0 N1)
    (Slt 1 N1)
    (Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647)))
    (Ult (ReadLSB w64 56 A-data-stat) 65536)
    (Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))]
    (Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args])
    

    KLEAVER does not crash when we do not ask for a counterexample.

    I will try to figure out what is happening to KLEE by also looking into the core dump. I hope to find out something useful to fix the bug.

  • [LLVM] Make KLEE compile against LLVM 3.7

    [LLVM] Make KLEE compile against LLVM 3.7

    There are not that many changes in 3.7, so this should be quite easy to review.

    There is no llvm 3.7 in travis to enable builds for. This 3.7 code is used by my llvm_38 port where I also enable build with llvm 3.8.

  • Restructured include/klee/

    Restructured include/klee/

    I think the Internal directory makes no sense, and having Module, Support directly under include/klee makes more sense. The patch changes lots of files but it's quite trivial.

  • Module/RaiseAsm: Support x86 (aka 32bit) as well

    Module/RaiseAsm: Support x86 (aka 32bit) as well

    Summary:

    Fixes:

    $ cat test.c
    int main(void) {}
    $ clang -m32 -emit-llvm -c test.c -o test.bc
    $ klee test.bc
    KLEE: output directory is "/home/lukas/klee/klee-out-9"
    KLEE: Using Z3 solver backend
    LLVM ERROR: 64-bit code requested on a subtarget that doesn't support it!
     #0 0x00007fb59688bbf6 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib64/libLLVM-12.so+0xc07bf6)
     #1 0x00007fb596889ae4 llvm::sys::RunSignalHandlers() (/lib64/libLLVM-12.so+0xc05ae4)
     #2 0x00007fb596889c69 (/lib64/libLLVM-12.so+0xc05c69)
     #3 0x00007fb595772310 __restore_rt (/lib64/libc.so.6+0x3d310)
     #4 0x00007fb595772292 raise (/lib64/libc.so.6+0x3d292)
     #5 0x00007fb59575b8a4 abort (/lib64/libc.so.6+0x268a4)
     #6 0x00007fb5967d7b5e llvm::report_fatal_error(llvm::Twine const&, bool) (/lib64/libLLVM-12.so+0xb53b5e)
     #7 0x00007fb5967d7c8e (/lib64/libLLVM-12.so+0xb53c8e)
     #8 0x00007fb5990e1b26 (/lib64/libLLVM-12.so+0x345db26)
     #9 0x00007fb5990e2120 (/lib64/libLLVM-12.so+0x345e120)
    #10 0x00007fb5990e5ac4 (/lib64/libLLVM-12.so+0x3461ac4)
    #11 0x00000000004919ed klee::RaiseAsmPass::runOnModule(llvm::Module&) /home/lukas/klee/build/../lib/Module/RaiseAsm.cpp:102:31
    #12 0x00007fb5969b1d02 llvm::legacy::PassManagerImpl::run(llvm::Module&) (/lib64/libLLVM-12.so+0xd2dd02)
    #13 0x0000000000486cac klee::KModule::instrument(klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Module/KModule.cpp:237:23
    #14 0x000000000043562f klee::Executor::setModule(std::vector<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> >, std::allocator<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> > > >&, klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Core/Executor.cpp:537:23
    #15 0x0000000000417dd5 main /home/lukas/klee/build/../tools/klee/main.cpp:1411:46
    #16 0x00007fb59575cb75 __libc_start_main (/lib64/libc.so.6+0x27b75)
    #17 0x0000000000424d6e _start (build/bin/klee+0x424d6e)
    

    Checklist:

    • [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [x] Each commit has a meaningful message documenting what it does.
    • [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [x] The code is commented OR not applicable/necessary.
    • [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [ ] There are test cases for the code you added or modified OR no such test cases are required.
  • ExecutorTimers: replace signalling with synchronous checks

    ExecutorTimers: replace signalling with synchronous checks

    Prevent endless looping fork in STPSolver (fixes #831) by replacing the signal-based timer handling with synchronous checks.

    Removes -max-instruction-time and introduces -timer-interval (default 1s).

  • Various updates to gen-random-bout.cpp

    Various updates to gen-random-bout.cpp

    This is to keep it up-to-date with the current ktest format, so that the output can be used as a seed.

    • Added handling of --sym-arg
    • Resolved the crash when minimum and maximum number of arguments for --sym-args are equal
    • Replaced range with n_args produced by --sym-args
    • Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input
    • Allow a single dash to prefix an option
    • Arrange the elements in the correct order: command-line arguments, files, stdin, and lastly stdout
  • klee assertion at IndependentSolver.cpp:545

    klee assertion at IndependentSolver.cpp:545

    klee (with llvm 3.4) is consistently asserting (after a few hours) at the following point:

    klee: IndependentSolver.cpp:545: virtual bool IndependentSolver::computeInitialValues(const klee::Query&, const std::vector<const klee::Array*>&, std::vector<std::vector >&, bool&): Assertion `assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && "should satisfy the equation"' failed.

    It looks like klee is trying to fork a new branch, but the initial path constraint is false. Can anyone tell me if this is indeed the fault?

    Also, any suggestions about what I might do about it?

    Thanks! Rick Rutledge

    byte code is attached, and klee ran with the following command line:

    klee -libc=uclibc -posix-runtime -entry-point=klee_main main.bc

    main.bc.zip

  • Dumping stack variables of custom functions

    Dumping stack variables of custom functions

    I'm trying to dump stack variables inside all functions interpreted by KLEE. I adopted the function void ExecutionState::dumpStack(std::ostream &out) taken from Here. However, KLEE doesn't return/dump all functions that have been executed. Therefore, I can't get the stack variables that belong to the missed functions. Though I'm not using any optimizations to perform function inlining. The attached file contains a simple example, the bitcode, and the script for running KLEE. In this example, the stack doesn't contain any info about the function set_pool_val, as shown below

    Stack: 
    	#000009004 in __klee_posix_wrapped_main ()
    	#100007257 in __user_main (=1, =94205840818176, =94205840818192) at /runtime/POSIX/klee_init_env.c:245
    	#200000525 in __uClibc_main (=94205841642760, =1, =94205840818176, =0, =0, =0, =0) at libc/misc/internals/__uClibc_main.c:401
    	#300000692 in main (=1, =94205840818176)
    Stack: 
    	#000009004 in __klee_posix_wrapped_main ()
    	#100007257 in __user_main (=1, =94231811603968, =94231811603984) at /runtime/POSIX/klee_init_env.c:245
    	#200000525 in __uClibc_main (=94231812429064, =1, =94231811603968, =0, =0, =0, =0) at libc/misc/internals/__uClibc_main.c:401
    	#300000692 in main (=1, =94231811603968)
    

    mimicNgx.zip

  • Implement a CMake based build system for KLEE.

    Implement a CMake based build system for KLEE.

    This is based off intial work by @jirislaby in #481. However it has been substantially modified.

    Notably it includes a separate build sytem to build the runtimes which is inspired by the old build system. The reason for doing this is because CMake is not well suited for building the runtime:

    • CMake is configured to use the host compiler, not the bitcode compiler. These are not the same thing.

    • Building the runtime using add_custom_command() is flawed because we can't automatically get transitive depencies (i.e. header file dependencies) unless the CMake generator is makefiles.

    So for now we have a very simple build system for building the runtimes. In the future we can replace this with something more sophisticated if we need it.

    Support for all important features of the old build system are implemented.

    Another notable change is the CMake build system works much better with LLVM installs which don't ship with testing tools. The build system will download the sources for FileCheck and not tools if the corresponding binaries aren't available and will build them. However lit (availabe via pip install lit) and GTest must already be installed.

    Apart from better support testing a significant advantage of the new CMake build system compared to the existing "Autoconf/Makefile" build system is that it is not coupled to LLVM's build system (unlike the existing build system).

    Currently all tests pass when building with STP, Z3 or metaSMT. I've only tried STP with different LLVM version (2.9 and 3.4). The other solvers I only tested with LLVM 3.4.

    I also quickly tried using Ninja as the CMake generator rather than "UNIX Makefiles" and the build seemed to work okay :)

  • Intrinsics: Add support for `@llvm.f{ma,muladd}.f*`

    Intrinsics: Add support for `@llvm.f{ma,muladd}.f*`

    Summary:

    Add support for llvm.fma and llvm.fmuladd intrinsics.

    Checklist:

    • [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [x] Each commit has a meaningful message documenting what it does.
    • [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [x] The code is commented OR not applicable/necessary.
    • [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [x] There are test cases for the code you added or modified OR no such test cases are required.
  • Upgrade build script/ Docker images to Ubuntu 22.04

    Upgrade build script/ Docker images to Ubuntu 22.04

    This issue is intended to tie together a couple of PRs/issues. Instead of polluting the each of the PRs, I'm going to comment here.

    Currently a couple of PRs are hold back because of the older Ubuntu version, therefore I would suggest to upgrade to a newer one. Most recent stable is 22.04, this might help us in the long run.

    Following PRs are related (afaik):

    • C++17 support: #1479
    • Support for LLVM 14: #1477

    Following plan:

    • [ ] Merge #1378
    • [ ] Remove support for LLVM <9
    • [ ] Upgrade to new Docker images, i.e. upgrade build scripts to support newer version
    • [ ] Merge #1477
    • [ ] Merge #1479
    • [ ] Upgrade to newer CMake and ease the pain for STP: https://github.com/stp/stp/issues/375#issuecomment-889178863

    Any other suggestions/comments?

  • .err files: minor readability changes to stack trace output

    .err files: minor readability changes to stack trace output

    Beforehand the stack traces in .err files looked a bit odd:

    	#000000026 in foo (i, k=12) at test.c:7 // with symbol names
    	#100000050 in main () at test.c:15
    

    or

    	#000000025 in foo (, =12) at test.c:7 // without symbol names
    	#100000048 in main () at test.c:15
    

    I've slightly modified it to:

    	#000000026 in foo(i=symbolic, k=12) at test.c:7
    	#100000050 in main() at test.c:15
    

    and

    	#000000025 in foo(symbolic, 12) at test.c:7
    	#100000048 in main() at test.c:15
    

    Summary:

    Checklist:

    • [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [x] Each commit has a meaningful message documenting what it does.
    • [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [x] The code is commented OR not applicable/necessary.
    • [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [x] There are test cases for the code you added or modified OR no such test cases are required.
  • `ConstantArrayExprVisitor`: Fix detection of multiple array indices

    `ConstantArrayExprVisitor`: Fix detection of multiple array indices

    Summary:

    Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the incompatible flag would not be set.

    Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected:

    if ((array1[k] + array2[x] + array2[k]) == 0)
    

    Resulting in the following output:

    KLEE: WARNING: OPT_I: infeasible branch!
    KLEE: WARNING: OPT_I: successful
    

    EDIT: major description rewrite so that it's much easier to understand the initial problem

    Checklist:

    • [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [x] Each commit has a meaningful message documenting what it does.
    • [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [x] The code is commented OR not applicable/necessary.
    • [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [x] There are test cases for the code you added or modified OR no such test cases are required.
  • Support arguments of width 128, 256 and 512 bits for external calls

    Support arguments of width 128, 256 and 512 bits for external calls

    Summary:

    Extend the maximum width of arguments and return values up to 512 bits in order to accept SIMD vectors.

    Closes #1488.

    Checklist:

    • [ x ] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [ x ] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [ x ] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [ x ] Each commit has a meaningful message documenting what it does.
    • [ x ] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [ x ] The code is commented OR not applicable/necessary.
    • [ x ] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [ x ] There are test cases for the code you added or modified OR no such test cases are required.
  • Spelling Fixes

    Spelling Fixes

    Summary:

    Fixes the spelling of some words that I found throughout the comments and code of the project. Has no effect on the program execution, just for the sake of clarity.

    Checklist:

    • [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
    • [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
    • [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
    • [x] Each commit has a meaningful message documenting what it does.
    • [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
    • [x] The code is commented OR not applicable/necessary.
    • [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
    • [x] There are test cases for the code you added or modified OR no such test cases are required.
Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework
Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework

About Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework. It provides various functionalities such as symbolic execution,

May 20, 2022
SANM: A Symbolic Asymptotic Numerical Solver

SANM: A Symbolic Asymptotic Numerical Solver This repository is the official implementation of the SANM solver described in our paper to appear at SIG

Apr 28, 2022
Metamath - Meta mathematics. Symbolic functions and derivatives.

metamath Meta mathematic metamath is a tiny header-only library. It can be used for symbolic computations on single-variable functions, such as dynami

Mar 3, 2022
Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE)
Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE)

Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE). The current release supports Intel ® SGX while other TEEs may be supported in future releases. Linux is also a supported target, though only suitable for testing purposes as it provides no additional protection.

May 19, 2022
PoC for CVE-2021-28476 a guest-to-host "Hyper-V Remote Code Execution Vulnerability" in vmswitch.sys.
PoC for CVE-2021-28476 a guest-to-host

CVE-2021-28476: a guest-to-host "Microsoft Hyper-V Remote Code Execution Vulnerability" in vmswitch.sys. This is a proof of concept for CVE-2021-28476

May 14, 2022
A refactored Proof-of-concept originally developed in 2017 to print all function calls with their arguments data types and values using Ptrace during program execution.

print-function-args-debugger A refactored Proof-of-concept originally developed in 2017 to print all function calls with their arguments data types an

Apr 19, 2022
x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration
x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration

anycall x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration Read: https://www.godeye.club/2021/05/14/0

May 9, 2022
May 13, 2022
New lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking code execution.
New lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking code execution.

BOF - Lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking ServiceMove is a POC code for an interestin

Apr 26, 2022
Elven relativism -- relocation and execution of aarch64 ELF relocatable objects (REL)
Elven relativism -- relocation and execution of aarch64 ELF relocatable objects (REL)

elvenrel Elven Relativism -- relocation and execution of aarch64 ELF relocatable objects (REL) on Linux and macOS. Program loads a multitude of ELF RE

Nov 28, 2021
RR4J is a tool that records java execution and later allows developers to replay locally.
RR4J is a tool that records java execution and later allows developers to replay locally.

RR4J [Record Replay 4 Java] RR4J is a tool that records java execution and later allows developers to replay locally. The tool solves one of the chall

Mar 15, 2022
CPU Performance Evaluation and Execution Time Prediction Using Narrow Spectrum Benchmarking

This is a simple implementation of Saavedra-Barrera's paper SAAVEDRA-BARRERA R H. CPU Performance Evaluation and Execution Time Prediction Using Narrow Spectrum Benchmarking[D/OL]. UCB/CSD92-684. EECS Department, University of California, Berkeley, 1992.

Jan 27, 2022
A Windows user-mode shellcode execution tool that demonstrates various techniques that malware uses
A Windows user-mode shellcode execution tool that demonstrates various techniques that malware uses

Jektor Toolkit v1.0 This utility focuses on shellcode injection techniques to demonstrate methods that malware may use to execute shellcode on a victi

Apr 28, 2022
Inject dll to cmd.exe to prevent file execution.

Console-Process-Execution Inject dll to cmd.exe to prevent file execution. Requierments: Microsoft Detours Library - https://github.com/microsoft/Deto

Dec 19, 2021
A pre-boot execution environment for Apple boards built on top of checkra1n

archOS A pre-boot execution environment for Apple boards built on top of checkra1n - currently based off the Checkra1n/PongoOS Repo. Building on macOS

Jan 17, 2022
This is a very short tool that predicts the number of cycles and execution time in Fulcrum when the operands and operations are known.

fulcrum-analytical-tool This is a very short tool that predicts the number of cycles and execution time in Fulcrum when the operands and operations ar

Feb 6, 2022
A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.).
A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.).

vmp_runner A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.) based on Unicorn. 一个基于Unicorn模拟执行虚拟化指令(vmpro

Apr 15, 2022
Love 6's Regular Expression Engine. Support Concat/Select/Closure Basic function. Hope u can enjoy this tiny engine :)
Love 6's Regular Expression Engine. Support Concat/Select/Closure Basic function. Hope u can enjoy this tiny engine :)

Regex_Engine Love 6's Blog Website: https://love6.blog.csdn.net/ Love 6's Regular Expression Engine Hope u can love my tiny regex engine :) maybe a fe

Apr 24, 2022
Sword Engine is a fork of Psych Engine that plans on adding more features and quality of life improvements.
Sword Engine is a fork of Psych Engine that plans on adding more features and quality of life improvements.

⚠️ WARNING: This README is currently incomplete, This warning will be removed once it's complete. Friday Night Funkin' - Sword Engine Sword Engine is

Mar 13, 2022