Giter VIP home page Giter VIP logo

symbisect's Introduction

SymBisect

To do

Feature

  • handle some the Linux kernel functions, e.g., kmalloc()
  • under constraint symbolic execution
  • terminate state at low priority basic block and stop at target basic block, which could be set in config json
  • handle indirect function call by MLTA default, also accept specify callee from config json
  • easily expanded, just inherit class Listener and add it in function preparation()

Build

sudo apt install -y git cmake vim curl make unzip
sudo apt install -y autoconf automake libtool g++ build-essential pkg-config flex bison 
sudo apt install -y libgflags-dev libgtest-dev libc++-dev libssl-dev libelf-dev libsqlite3-dev

build with apt install llvm & z3 (sudo)

sudo apt install llvm-11 clang-11 z3
mkdir ./cmake-build
cd ./cmake-build
cmake -DCMAKE_BUILD_TYPE=Debug \
  -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-11 \
  -DENABLE_SOLVER_Z3=ON \
  -DENABLE_UNIT_TESTS=OFF \
  -DENABLE_SYSTEM_TESTS=OFF \
  -DENABLE_TCMALLOC=OFF \
  -DENABLE_DOXYGEN=OFF \
  -G "CodeBlocks - Unix Makefiles" \
  ..
make -j

build llvm & z3 & klee (no sudo)

export PATH_PROJECT=$PWD
mkdir $PATH_PROJECT/build
mkdir $PATH_PROJECT/install

# build llvm & clang
cd $PATH_PROJECT/build
git clone https://github.com/llvm/llvm-project.git
cd llvm-project
git checkout tags/llvmorg-11.0.0
mkdir build && cd build
cmake -G "Unix Makefiles" \
  -DCMAKE_BUILD_TYPE=Release \
  -DLLVM_ENABLE_PROJECTS="clang;lld" \
  -DLLVM_TARGETS_TO_BUILD="X86" \
  -DCMAKE_INSTALL_PREFIX=$PATH_PROJECT/install \
  ../llvm
make -j10
make install

# build z3
cd $PATH_PROJECT/build
git clone [email protected]:Z3Prover/z3.git
cd z3
git checkout z3-4.8.9
python3 scripts/mk_make.py --prefix=$PATH_PROJECT/install
cd build
make -j
make install

# build klee
mkdir $PATH_PROJECT/cmake-build
cd $PATH_PROJECT/cmake-build
cmake -DCMAKE_BUILD_TYPE=Debug \
  -DLLVM_CONFIG_BINARY=$PATH_PROJECT/install/bin/llvm-config \
  -DENABLE_SOLVER_Z3=ON \
  -DZ3_INCLUDE_DIRS=$PATH_PROJECT/install/include \
  -DZ3_LIBRARIES=$PATH_PROJECT/install/lib/libz3.so \
  -DENABLE_UNIT_TESTS=OFF \
  -DENABLE_SYSTEM_TESTS=OFF \
  -DENABLE_TCMALLOC=OFF \
  -DENABLE_DOXYGEN=OFF \
  -G "CodeBlocks - Unix Makefiles" \
  -DCMAKE_INSTALL_PREFIX=$PATH_PROJECT/install \
  ..
make -j
make install

# generate environment.sh
cd $PATH_PROJECT
echo "export PATH=$PATH_PROJECT/install/bin:\$PATH" >> environment.sh
echo "export PKG_CONFIG_PATH=$PATH_PROJECT/install/lib/pkgconfig:\$PKG_CONFIG_PATH" >> environment.sh
echo "export PATH_PROJECT=$PATH_PROJECT" >> environment.sh

Usage

klee --config=config.json

look at config.json to know more about the config json file.

symbisect's People

Contributors

zhyfeng avatar zhangzhenghsy avatar

Stargazers

xyz2k8 avatar

Watchers

avatar xyz2k8 avatar avatar avatar

Forkers

seclab-ucr

symbisect's Issues

Model of strncpy_from_user: could we create an object with a given address?

long strncpy_from_user(char *dst, const char __user *src, long count)
(https://elixir.bootlin.com/linux/v5.5-rc5/source/lib/strncpy_from_user.c#L104)
copies a buf from userspace to a given address dst
the buf can be tail of a struct ( struct file_name for example, https://elixir.bootlin.com/linux/v5.5-rc5/source/include/linux/fs.h#L2517)
we symbolize the struct but the size of buf is not counted, thus the dst address doesn't belong to any object

I want to model it
It seems that when we create an object in UCKLEE (Executor::create_mo, memory->allocate), we cannot control the address of the object
How could we solve it?

My current thinking is that if the address is adjacent to an existing object (struct file_name in the above example), we found it can extend the size of it
if we cannot find such a object, then we make a mapping between the given concrete address and real object address?

test case: /home/zzhan173/repos/Linux_kernel_UC_KLEE/configs/getname_flags_cover_func.json

Symbolize global variables

Currently some global variables in llvm bc files are initialized to Null, it will result in some incorrect results
For example, in file_system_type() function ( https://elixir.bootlin.com/linux/v5.5-rc5/source/fs/filesystems.c#L52 )
file_systems is null in the bc file, and the loop will be skipped and null pointer is returned directly. It will terminate the following execution

Currently, let's symbolize the global variables which equal null first? Maybe we need to symbolize more global variables later

test case, /home/zzhan173/repos/Linux_kernel_UC_KLEE/configs/find_filesystem.json

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.