From 6356d8ef7ba3c8f05513768caf25042f9288896b Mon Sep 17 00:00:00 2001 From: Adrian Herrera Date: Sun, 30 Dec 2018 23:03:00 +1100 Subject: [PATCH] added S2E support --- CMakeLists.txt | 48 ++++- README.md | 17 +- bin/deepstate/main_s2e.py | 77 +++++++ bin/deepstate/s2e/__init__.py | 0 bin/deepstate/s2e/project.py | 203 ++++++++++++++++++ bin/deepstate/s2e/templates/__init__.py | 0 bin/deepstate/s2e/templates/bootstrap.sh.j2 | 58 +++++ bin/deepstate/s2e/templates/launch-s2e.sh.j2 | 35 +++ bin/deepstate/s2e/templates/s2e-config.lua.j2 | 62 ++++++ bin/setup.py.in | 1 + examples/CMakeLists.txt | 65 +++++- src/lib/DeepState.c | 72 ++++++- src/lib/Log.c | 8 + src/lib/Stream.c | 40 ++++ 14 files changed, 671 insertions(+), 15 deletions(-) create mode 100644 bin/deepstate/main_s2e.py create mode 100644 bin/deepstate/s2e/__init__.py create mode 100644 bin/deepstate/s2e/project.py create mode 100644 bin/deepstate/s2e/templates/__init__.py create mode 100644 bin/deepstate/s2e/templates/bootstrap.sh.j2 create mode 100644 bin/deepstate/s2e/templates/launch-s2e.sh.j2 create mode 100644 bin/deepstate/s2e/templates/s2e-config.lua.j2 diff --git a/CMakeLists.txt b/CMakeLists.txt index 448dfa73..191aed6b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -114,13 +114,13 @@ if (BUILD_LIBFUZZER) src/lib/Option.c src/lib/Stream.c ) - + target_compile_options(${PROJECT_NAME}_LF PUBLIC -DLIBFUZZER -mno-avx -fsanitize=fuzzer-no-link,undefined) - + target_include_directories(${PROJECT_NAME}_LF PUBLIC SYSTEM "${CMAKE_SOURCE_DIR}/src/include" ) - + install( TARGETS ${PROJECT_NAME} ${PROJECT_NAME}_LF LIBRARY DESTINATION lib @@ -128,6 +128,48 @@ if (BUILD_LIBFUZZER) ) endif() +if (NOT DEFINED BUILD_S2E AND DEFINED ENV{BUILD_S2E}) + set(BUILD_S2E "$ENV{BUILD_S2E}") +endif() + +if (BUILD_S2E) + if (NOT DEFINED S2E_ENV_PATH AND DEFINED ENV{S2EDIR}) + SET(S2E_ENV_PATH "$ENV{S2EDIR}") + endif() + + GET_FILENAME_COMPONENT(S2E_ENV_PATH ${S2E_ENV_PATH} ABSOLUTE) + if ("${S2E_ENV_PATH}" STREQUAL "") + message(FATAL_ERROR "S2E support enabled but S2E environment path not provided." + " Please activate your S2E environment or set S2E_ENV_PATH") + endif () + + set(S2E_INCLUDE "${S2E_ENV_PATH}/source/s2e/guest/common/include") + if (EXISTS "${S2E_INCLUDE}/s2e/s2e.h") + message(STATUS "Valid S2E environment found at ${S2E_ENV_PATH}") + else () + message(FATAL_ERROR "s2e.h not found in ${S2E_INCLUDE}/s2e. Are you sure that this is a valid S2E environment?") + endif () + + add_library(${PROJECT_NAME}_S2E STATIC + src/lib/DeepState.c + src/lib/Log.c + src/lib/Option.c + src/lib/Stream.c + ) + + target_compile_options(${PROJECT_NAME}_S2E PUBLIC -DBUILD_S2E) + + target_include_directories(${PROJECT_NAME}_S2E + PUBLIC SYSTEM "${CMAKE_SOURCE_DIR}/src/include" + PUBLIC SYSTEM "${S2E_INCLUDE}" + ) + + install( + TARGETS ${PROJECT_NAME} ${PROJECT_NAME}_S2E + LIBRARY DESTINATION lib + ARCHIVE DESTINATION lib + ) +endif() set(SETUP_PY_IN "${CMAKE_SOURCE_DIR}/bin/setup.py.in") set(SETUP_PY "${CMAKE_CURRENT_BINARY_DIR}/setup.py") diff --git a/README.md b/README.md index cf5420c0..4a33394d 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ The [2018 IEEE Cybersecurity Development Conference](https://secdev.ieee.org/201 * Tests look like Google Test, but can use symbolic execution/fuzzing to generate data (parameterized unit testing) * Easier to learn than binary analysis tools/fuzzers, but provides similar functionality -* Already supports Manticore, Angr, libFuzzer, file-based fuzzing with e.g., AFL; more back-ends likely in future +* Already supports Manticore, Angr, libFuzzer, S2E, file-based fuzzing with e.g., AFL; more back-ends likely in future * Switch test generation tool without re-writing test harness * Work around show-stopper bugs * Find out which tool works best for your code under test @@ -296,6 +296,21 @@ Because AFL and other file-based fuzzers only rely on the DeepState native test executable, they should (like DeepState's built-in simple fuzzer) work fine on macOS and other Unix-like OSes. +## Test-case Generation with S2E + +To enable S2E support, run CMake with the following options: + +```shell +cmake -DBUILD_S2E=On -DS2E_ENV_PATH=/path/to/s2e/environment ../ +``` + +Where `S2E_ENV_PATH` is a path to an S2E environment created with [s2e-env](https://github.com/S2E/s2e-env). + +The `deepstate-s2e` command will create analysis projects in your S2E +environment. You can then start the S2E analysis by running `launch-s2e.sh`. +Once the analysis completes tests will be available in the `s2e-last/tests/` +directory. + ## Contributing All accepted PRs are awarded bounties by Trail of Bits. Join the #deepstate channel on the [Empire Hacking Slack](https://empireslacking.herokuapp.com/) to discuss ongoing development and claim bounties. Check the [good first issue](https://github.com/trailofbits/deepstate/issues?q=is%3Aissue+is%3Aopen+label%3A%22good+first+issue%22) label for suggested contributions. diff --git a/bin/deepstate/main_s2e.py b/bin/deepstate/main_s2e.py new file mode 100644 index 00000000..18260423 --- /dev/null +++ b/bin/deepstate/main_s2e.py @@ -0,0 +1,77 @@ +#!/usr/bin/env python +# Copyright (c) 2018 Adrian Herrera +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +import logging +import os + +from s2e_env.manage import call_command +from s2e_env.commands.new_project import Command as NewProjectCommand +from s2e_env.utils import log as s2e_log + +from deepstate.common import LOG_LEVEL_DEBUG, LOG_LEVEL_TRACE, LOG_LEVEL_INFO, \ + LOG_LEVEL_WARNING, LOG_LEVEL_ERROR, LOG_LEVEL_FATAL +from .common import DeepState +from .s2e.project import DeepStateProject + + +L = logging.getLogger("deepstate.s2e") +L.setLevel(logging.INFO) + +LOG_LEVEL_TO_LOGGING_LEVEL = { + LOG_LEVEL_DEBUG: logging.DEBUG, + LOG_LEVEL_TRACE: 15, + LOG_LEVEL_INFO: logging.INFO, + LOG_LEVEL_WARNING: logging.WARNING, + LOG_LEVEL_ERROR: logging.ERROR, + LOG_LEVEL_FATAL: logging.CRITICAL, +} + + +def get_s2e_env(): + s2e_env_dir = os.getenv("S2EDIR") + if not s2e_env_dir: + raise Exception("S2EDIR environment variable not specified. Ensure " + "that s2e_activate.sh has been sourced") + if not os.path.isdir(s2e_env_dir): + raise Exception("S2EDIR {} is invalid".format(s2e_env_dir)) + + return s2e_env_dir + + +def main(): + """ + Create an s2e-env project that is suitable for analyzing a DeepState test. + """ + args = DeepState.parse_args() + + # Sync S2E and DeepState logging levels + s2e_log.configure_logging(level=LOG_LEVEL_TO_LOGGING_LEVEL[args.verbosity]) + + try: + s2e_env_path = get_s2e_env() + proj_name = "{}-deepstate".format(os.path.basename(args.binary)) + + call_command(NewProjectCommand(), args.binary, env=s2e_env_path, + name=proj_name, project_class=DeepStateProject, + **vars(args)) + except Exception as e: + L.critical("Cannot create an S2E project for %s: %s", args.binary, e) + return 1 + + return 0 + + +if __name__ == '__main__': + exit(main()) diff --git a/bin/deepstate/s2e/__init__.py b/bin/deepstate/s2e/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/bin/deepstate/s2e/project.py b/bin/deepstate/s2e/project.py new file mode 100644 index 00000000..423b8fc8 --- /dev/null +++ b/bin/deepstate/s2e/project.py @@ -0,0 +1,203 @@ +# Copyright (c) 2018 Adrian Herrera +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + + +import datetime +import logging +import os +import shutil + +from s2e_env.command import CommandError +from s2e_env.commands.project_creation.abstract_project import AbstractProject +from s2e_env.utils.templates import render_template + + +L = logging.getLogger('deepstate.s2e') +L.setLevel(logging.INFO) + +# Only Linux targets are supported +ARCH_TO_IMAGE = { + 'i386': 'debian-9.2.1-i386', + 'x86_64': 'debian-9.2.1-x86_64', +} + +DEEPSTATE_TEMPLATES_DIR = os.path.join(os.path.dirname(__file__), 'templates') + +INSTRUCTIONS = """ +Your DeepState project is available in {project_dir}. + +This is a simplified version of a regular S2E analysis project. To start the +analysis: + + * cd {project_dir} && ./launch-s2e.sh + +This will run the DeepState-enabled program in an S2E guest VM. The generated +tests will appear in the s2e-last/tests directory. The tests can be run using +the `--input_test_files_dir` option on a **NON** S2E-compiled program (running +an S2E-compiled program **outside** of S2E will result in an illegal +instruction error). + +Customization +============= + +* By default, your analysis will run with {num_workers} worker(s). This can be + changed by modifying the S2E_MAX_PROCESSES variable in launch-s2e.sh +* If your target program depends on other files (e.g., shared libraries, etc.), + then these should be retrieved in bootstrap.sh by adding a call to ${{S2EGET}} +* Only the minimum plugins required to generate tests have been enabled. To + enable more, edit s2e-config.lua +""" + + +class DeepStateProject(AbstractProject): + """A simplified S2E analysis project for DeepState-compiled programs.""" + + def _configure(self, target, *args, **options): + """ + Generate the S2E analysis project configuration. + """ + if target.is_empty(): + raise CommandError('Cannot use an empty target for a DeepState ' + 'project') + + # Decide on the image to use + image = ARCH_TO_IMAGE.get(target.arch) + if not image: + raise CommandError('Unable to find a suitable image for %s' % + target.path) + img_desc = self._select_image(target, image, download_image=False) + L.info('Using %s', img_desc['name']) + + # Determine if guestfs is available for this image + guestfs_path = self._select_guestfs(img_desc) + if not guestfs_path: + L.warn('No guestfs available. The VMI plugin may not run optimally') + + # Return the project config dict + return { + 'creation_time': str(datetime.datetime.now()), + 'project_dir': self.env_path('projects', options['name']), + 'image': img_desc, + 'has_guestfs': guestfs_path is not None, + 'guestfs_path': guestfs_path, + 'target_path': target.path, + 'target_arch': target.arch, + 'num_workers': options['num_workers'], + } + + def _create(self, config, force=False): + """ + Create the S2E analysis project, based on the given configuration. + """ + project_dir = config['project_dir'] + + # The force option is not exposed on the command-line for a DeepState + # project, so fail if the project directory already exists + if os.path.isdir(project_dir): + raise CommandError('Project directory %s already exists' % + project_dir) + + os.mkdir(project_dir) + + try: + # Create a symlink to the analysis target + self._symlink_project_files(project_dir, config['target_path']) + + # Create a symlink to the guest tools directory + self._symlink_guest_tools(project_dir, config['image']) + + # Create a symlink to the guestfs (if it exists) + if config['guestfs_path']: + self._symlink_guestfs(project_dir, config['guestfs_path']) + + # Render the templates + self._create_launch_script(project_dir, config) + self._create_lua_config(project_dir, config) + self._create_bootstrap(project_dir, config) + except Exception: + # If anything goes wrong during project creation, remove anything + # incomplete + shutil.rmtree(project_dir) + raise + + return project_dir + + def _get_instructions(self, config): + """ + Generate instructions. + """ + return INSTRUCTIONS.format(**config) + + def _create_launch_script(self, project_dir, config): + """ + Create the S2E launch script. + """ + L.info('Creating launch script') + + img_desc = config['image'] + context = { + 'creation_time': config['creation_time'], + 'env_dir': self.env_path(), + 'rel_image_path': os.path.relpath(img_desc['path'], self.env_path()), + 'max_processes': config['num_workers'], + 'qemu_arch': img_desc['qemu_build'], + 'qemu_memory': img_desc['memory'], + 'qemu_snapshot': img_desc['snapshot'], + 'qemu_extra_flags': img_desc['qemu_extra_flags'], + } + + output_file = 'launch-s2e.sh' + output_path = os.path.join(project_dir, output_file) + + render_template(context, '%s.j2' % output_file, output_path, + templates_dir=DEEPSTATE_TEMPLATES_DIR, executable=True) + + def _create_lua_config(self, project_dir, config): + """ + Create the S2E Lua config. + """ + L.info('Creating S2E configuration') + + self._copy_lua_library(project_dir) + + context = { + 'creation_time': config['creation_time'], + 'project_dir': config['project_dir'], + 'target_process': os.path.basename(config['target_path']), + 'has_guestfs': config['has_guestfs'], + 'guestfs_path': config['guestfs_path'], + } + + output_file = 's2e-config.lua' + output_path = os.path.join(project_dir, output_file) + + render_template(context, '%s.j2' % output_file, output_path, + templates_dir=DEEPSTATE_TEMPLATES_DIR) + + def _create_bootstrap(self, project_dir, config): + """ + Create the S2E bootstrap script. + """ + L.info('Creating S2E bootstrap script') + + context = { + 'creation_time': config['creation_time'], + 'target': os.path.basename(config['target_path']), + } + + output_file = 'bootstrap.sh' + output_path = os.path.join(project_dir, output_file) + + render_template(context, '%s.j2' % output_file, output_path, + templates_dir=DEEPSTATE_TEMPLATES_DIR) diff --git a/bin/deepstate/s2e/templates/__init__.py b/bin/deepstate/s2e/templates/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/bin/deepstate/s2e/templates/bootstrap.sh.j2 b/bin/deepstate/s2e/templates/bootstrap.sh.j2 new file mode 100644 index 00000000..2defd458 --- /dev/null +++ b/bin/deepstate/s2e/templates/bootstrap.sh.j2 @@ -0,0 +1,58 @@ +#!/bin/bash +# +# This file was automatically generated by DeepState at {{ creation_time }} +# +# This bootstrap script is used to control the execution of the target program +# in an S2E guest VM. It is a simplified version of s2e-env's bootstrap.sh. +# + +set -x + +# Useful variables +S2ECMD=./s2ecmd +S2EGET=./s2eget +S2EPUT=./s2eput + +TARGET="{{ target }}" + +# Don't print crashes in the syslog. This prevents unnecessary forking in the +# kernel +sudo sysctl -w debug.exception-trace=0 + +# Prevent core dumps from being created. This prevents unnecessary forking in +# the kernel +ulimit -c 0 + +# Ensure that /tmp is mounted in memory (if you built the image using s2e-env +# then this should already be the case. But better to be safe than sorry!) +if ! mount | grep "/tmp type tmpfs"; then + sudo mount -t tmpfs -osize=10m tmpfs /tmp +fi + +# Disable swap, otherwise there will be forced concretization if the system +# swaps out symbolic data to disk. +sudo swapoff -a + +# Start the LinuxMonitor kernel module +sudo modprobe s2e + +# Update the guest tools +GUEST_TOOLS="s2ecmd s2eget s2eput s2e.so" +for TOOL in ${GUEST_TOOLS}; do + ${S2EGET} guest-tools/${TOOL} + chmod +x ${TOOL} +done + +# Download the target file to analyze. If additional files are required, add +# them here +${S2EGET} ${TARGET} + +# Make sure that the target is executable +chmod +x ${TARGET} + +# Execute the target. stdout and stderr are redirected to avoid concretization +# when printing symbolic values +./${TARGET} > /dev/null 2> /dev/null + +# Kill states before exiting +${S2ECMD} kill $? "Target execution terminated" diff --git a/bin/deepstate/s2e/templates/launch-s2e.sh.j2 b/bin/deepstate/s2e/templates/launch-s2e.sh.j2 new file mode 100644 index 00000000..f88759e8 --- /dev/null +++ b/bin/deepstate/s2e/templates/launch-s2e.sh.j2 @@ -0,0 +1,35 @@ +#!/bin/bash +# +# This file was automatically generated by DeepState at {{ creation_time }} +# +# This script is used to run the S2E analysis. It is a simplified version of +# s2e-env's launch-s2e.sh. +# + +# Useful variables +ENV_DIR="{{ env_dir }}" +INSTALL_DIR="${ENV_DIR}/install" +THIS_DIR="$(dirname $(realpath -s ${0}))" +S2E_LAST="${THIS_DIR}/s2e-last" +TESTS_DIR="${S2E_LAST}/tests" + +export S2E_CONFIG="s2e-config.lua" +export S2E_SHARED_DIR="${INSTALL_DIR}/share/libs2e" +export S2E_MAX_PROCESSES="{{ max_processes }}" +export S2E_UNBUFFERED_STREAM="1" + +LIBS2E="${S2E_SHARED_DIR}/libs2e-{{ qemu_arch}}-s2e.so" +QEMU="${INSTALL_DIR}/bin/qemu-system-{{ qemu_arch }}" +DRIVE="-drive file=${ENV_DIR}/{{ rel_image_path }},format=s2e,cache=writeback" + +# Run S2E +LD_PRELOAD=${LIBS2E} ${QEMU} ${DRIVE} \ + -k en-us -nographic -monitor null -m {{ qemu_memory }} -enable-kvm \ + -serial file:serial.txt {{ qemu_extra_flags }} \ + -loadvm {{ qemu_snapshot }} + +# Copy out the tests +mkdir -p ${TESTS_DIR} +for TEST in ${S2E_LAST}/testcase-*; do + mv ${TEST} ${TESTS_DIR}/$(md5sum ${TEST} | cut -d ' ' -f 1) +done diff --git a/bin/deepstate/s2e/templates/s2e-config.lua.j2 b/bin/deepstate/s2e/templates/s2e-config.lua.j2 new file mode 100644 index 00000000..2e6eb965 --- /dev/null +++ b/bin/deepstate/s2e/templates/s2e-config.lua.j2 @@ -0,0 +1,62 @@ +--[[ +This file was automatically generated by DeepState at {{ creation_time }} + +This is the main S2E configuration file. It is a simplified version of +s2e-env's s2e-config.lua. +]]-- + +s2e = { + logging = { + -- One of "all", "debug", "info", "warn" or "none" + console = "info", + logLevel = "warn", + }, + kleeArgs = { + }, +} + +plugins = {} +pluginsConfig = {} + +dofile('library.lua') + +add_plugin("BaseInstructions") +pluginsConfig.BaseInstructions = { + logLevel = "info", +} + +add_plugin("HostFiles") +pluginsConfig.HostFiles = { + baseDirs = { "{{ project_dir }}" }, + allowWrite = true, +} + +add_plugin("Vmi") +pluginsConfig.Vmi = { + baseDirs = { + "{{ project_dir }}", + {% if has_guestfs %} + "{{ guestfs_path }}", + {% endif %} + }, +} + +add_plugin("MemoryMap") + +add_plugin("ProcessExecutionDetector") +pluginsConfig.ProcessExecutionDetector = { + moduleNames = { "{{ target_process }}" }, +} + +add_plugin("LinuxMonitor") +pluginsConfig.LinuxMonitor = { + terminateOnSegfault = true, + terminateOnTrap = true, +} + +add_plugin("TestCaseGenerator") +pluginsConfig.TestCaseGeneratror = { + generateOnStateKill = true, + generateOnSegFault = true, + logLevel = "info", +} diff --git a/bin/setup.py.in b/bin/setup.py.in index f4a03e18..bf6a1e10 100644 --- a/bin/setup.py.in +++ b/bin/setup.py.in @@ -40,5 +40,6 @@ setuptools.setup( 'deepstate-angr = deepstate.main_angr:main', 'deepstate-manticore = deepstate.main_manticore:main', 'deepstate-reduce = deepstate.reducer:main', + 'deepstate-s2e = deepstate.main_s2e:main', ] }) diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index f8e7a215..de586f4f 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -16,92 +16,137 @@ add_executable(Crash Crash.cpp) target_link_libraries(Crash deepstate) if (BUILD_LIBFUZZER) - add_executable(Crash_LF Crash.cpp) + add_executable(Crash_LF Crash.cpp) target_link_libraries(Crash_LF deepstate_LF) target_link_libraries (Crash_LF "-fsanitize=fuzzer,undefined") set_target_properties(Crash_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() -add_executable(OneOf OneOf.cpp) +if (BUILD_S2E) + add_executable(Crash_S2E Crash.cpp) + target_link_libraries(Crash_S2E deepstate_S2E) +endif() + +add_executable(OneOf OneOf.cpp) target_link_libraries(OneOf deepstate) if (BUILD_LIBFUZZER) - add_executable(OneOf_LF OneOf.cpp) + add_executable(OneOf_LF OneOf.cpp) target_link_libraries(OneOf_LF deepstate_LF) target_link_libraries (OneOf_LF "-fsanitize=fuzzer,undefined") set_target_properties(OneOf_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(OneOf_S2E OneOf.cpp) + target_link_libraries(OneOf_S2E deepstate_S2E) +endif() + add_executable(Fixture Fixture.cpp) target_link_libraries(Fixture deepstate) if (BUILD_LIBFUZZER) - add_executable(Fixture_LF Fixture.cpp) + add_executable(Fixture_LF Fixture.cpp) target_link_libraries(Fixture_LF deepstate_LF) target_link_libraries (Fixture_LF "-fsanitize=fuzzer,undefined") set_target_properties(Fixture_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(Fixture_S2E Fixture.cpp) + target_link_libraries(Fixture_S2E deepstate_S2E) +endif() + add_executable(Primes Primes.cpp) target_link_libraries(Primes deepstate) if (BUILD_LIBFUZZER) - add_executable(Primes_LF Primes.cpp) + add_executable(Primes_LF Primes.cpp) target_link_libraries(Primes_LF deepstate_LF) target_link_libraries (Primes_LF "-fsanitize=fuzzer,undefined") set_target_properties(Primes_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(Primes_S2E Primes.cpp) + target_link_libraries(Primes_S2E deepstate_S2E) +endif() + add_executable(Euler Euler.cpp) target_link_libraries(Euler deepstate) if (BUILD_LIBFUZZER) - add_executable(Euler_LF Euler.cpp) + add_executable(Euler_LF Euler.cpp) target_link_libraries(Euler_LF deepstate_LF) target_link_libraries (Euler_LF "-fsanitize=fuzzer,undefined") set_target_properties(Euler_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(Euler_S2E Euler.cpp) + target_link_libraries(Euler_S2E deepstate_S2E) +endif() + add_executable(IntegerOverflow IntegerOverflow.cpp) target_link_libraries(IntegerOverflow deepstate) if (BUILD_LIBFUZZER) - add_executable(IntegerOverflow_LF IntegerOverflow.cpp) + add_executable(IntegerOverflow_LF IntegerOverflow.cpp) target_link_libraries(IntegerOverflow_LF deepstate_LF) target_link_libraries (IntegerOverflow_LF "-fsanitize=fuzzer,undefined") set_target_properties(IntegerOverflow_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(IntegerOverflow_S2E IntegerOverflow.cpp) + target_link_libraries(IntegerOverflow_S2E deepstate_S2E) +endif() + add_executable(IntegerArithmetic IntegerArithmetic.cpp) target_link_libraries(IntegerArithmetic deepstate) if (BUILD_LIBFUZZER) - add_executable(IntegerArithmetic_LF IntegerArithmetic.cpp) + add_executable(IntegerArithmetic_LF IntegerArithmetic.cpp) target_link_libraries(IntegerArithmetic_LF deepstate_LF) target_link_libraries (IntegerArithmetic_LF "-fsanitize=fuzzer,undefined") set_target_properties(IntegerArithmetic_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(IntegerArithmetic_S2E IntegerArithmetic.cpp) + target_link_libraries(IntegerArithmetic_S2E deepstate_S2E) +endif() + add_executable(Lists Lists.cpp) target_link_libraries(Lists deepstate) if (BUILD_LIBFUZZER) - add_executable(Lists_LF Lists.cpp) + add_executable(Lists_LF Lists.cpp) target_link_libraries(Lists_LF deepstate_LF) target_link_libraries (Lists_LF "-fsanitize=fuzzer,undefined") set_target_properties(Lists_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(Lists_S2E Lists.cpp) + target_link_libraries(Lists_S2E deepstate_S2E) +endif() + add_executable(StreamingAndFormatting StreamingAndFormatting.cpp) target_link_libraries(StreamingAndFormatting deepstate) if (BUILD_LIBFUZZER) - add_executable(StreamingAndFormatting_LF StreamingAndFormatting.cpp) + add_executable(StreamingAndFormatting_LF StreamingAndFormatting.cpp) target_link_libraries(StreamingAndFormatting_LF deepstate_LF) target_link_libraries (StreamingAndFormatting_LF "-fsanitize=fuzzer,undefined") set_target_properties(StreamingAndFormatting_LF PROPERTIES COMPILE_DEFINITIONS "LIBFUZZER") endif() +if (BUILD_S2E) + add_executable(StreamingAndFormatting_S2E StreamingAndFormatting.cpp) + target_link_libraries(StreamingAndFormatting_S2E deepstate_S2E) +endif() + if (NOT APPLE) add_executable(Squares Squares.c) target_link_libraries(Squares deepstate) diff --git a/src/lib/DeepState.c b/src/lib/DeepState.c index 411583a5..5b4f6582 100644 --- a/src/lib/DeepState.c +++ b/src/lib/DeepState.c @@ -23,6 +23,10 @@ #include #include +#ifdef BUILD_S2E +#include "s2e/s2e.h" +#endif + #ifdef DEEPSTATE_TAKEOVER_RAND #undef rand #undef srand @@ -126,17 +130,25 @@ DEEPSTATE_NORETURN void DeepState_Fail(void) { DeepState_SetTestFailed(); +#ifdef BUILD_S2E + s2e_kill_state(1, "[DeepState] Test failed"); +#else if (FLAGS_take_over) { // We want to communicate the failure to a parent process, so exit. exit(DeepState_TestRunFail); } else { longjmp(DeepState_ReturnToRun, 1); } +#endif } /* Mark this test as passing. */ DEEPSTATE_NORETURN void DeepState_Pass(void) { +#ifdef BUILD_S2E + struct DeepState_TestInfo *test = DeepState_CurrentTestRun->test; + DeepState_LogFormat(DeepState_LogInfo, "Passed: %s", test->test_name); +#endif longjmp(DeepState_ReturnToRun, 0); } @@ -154,6 +166,10 @@ void DeepState_SymbolizeData(void *begin, void *end) { } else if (begin_addr == end_addr) { return; } else { + uintptr_t length = end_addr - begin_addr; + if (DeepState_InputIndex + length >= DeepState_InputSize) { + DeepState_Abandon("Read too many symbols"); + } uint8_t *bytes = (uint8_t *) begin; for (uintptr_t i = 0, max_i = (end_addr - begin_addr); i < max_i; ++i) { if (DeepState_InputIndex >= DeepState_InputSize) { @@ -164,11 +180,20 @@ void DeepState_SymbolizeData(void *begin, void *end) { } bytes[i] = DeepState_Input[DeepState_InputIndex++]; } +#ifdef BUILD_S2E + s2e_make_symbolic((void*) bytes, length, "__symfile___deepstate_input___0_1_symfile__"); +#endif } } /* Concretize some data in exclusive the range `[begin, end)`. */ void *DeepState_ConcretizeData(void *begin, void *end) { +#ifdef BUILD_S2E + uintptr_t begin_addr = (uintptr_t) begin; + uintptr_t end_addr = (uintptr_t) end; + + s2e_concretize(begin, (end_addr - begin_addr)); +#endif return begin; } @@ -197,6 +222,9 @@ void DeepState_SymbolizeCStr(char *begin) { /* Concretize a C string */ const char *DeepState_ConcretizeCStr(const char *begin) { +#ifdef BUILD_S2E + s2e_concretize((void*) begin, strlen(begin)); +#endif return begin; } @@ -244,6 +272,7 @@ int DeepState_Bool(void) { return DeepState_Input[DeepState_InputIndex++] & 1; } +#ifdef BUILD_S2E #define MAKE_SYMBOL_FUNC(Type, type) \ type DeepState_ ## Type(void) { \ if ((DeepState_InputIndex + sizeof(type)) > DeepState_InputSize) { \ @@ -263,9 +292,33 @@ int DeepState_Bool(void) { if (FLAGS_verbose_reads) { \ printf("FINISHED MULTI-BYTE READ\n"); \ } \ + s2e_make_symbolic(&val, sizeof(type), \ + "__symfile___deepstate_input_" DEEPSTATE_TO_STR(Type) "___0_1_symfile__"); \ return val; \ } - +#else +#define MAKE_SYMBOL_FUNC(Type, type) \ + type DeepState_ ## Type(void) { \ + if ((DeepState_InputIndex + sizeof(type)) > DeepState_InputSize) { \ + DeepState_Abandon("Read too many symbols"); \ + } \ + type val = 0; \ + if (FLAGS_verbose_reads) { \ + printf("STARTING MULTI-BYTE READ\n"); \ + } \ + _Pragma("unroll") \ + for (size_t i = 0; i < sizeof(type); ++i) { \ + if (FLAGS_verbose_reads) { \ + printf("Reading byte at %u\n", DeepState_InputIndex); \ + } \ + val = (val << 8) | ((type) DeepState_Input[DeepState_InputIndex++]); \ + } \ + if (FLAGS_verbose_reads) { \ + printf("FINISHED MULTI-BYTE READ\n"); \ + } \ + return val; \ + } +#endif MAKE_SYMBOL_FUNC(Size, size_t) @@ -298,6 +351,9 @@ int32_t DeepState_RandInt() { /* Returns the minimum satisfiable value for a given symbolic value, given * the constraints present on that value. */ uint32_t DeepState_MinUInt(uint32_t v) { +#ifdef BUILD_S2E + DeepState_Abandon("MinUInt not yet supported by S2E"); +#endif return v; } @@ -309,6 +365,9 @@ int32_t DeepState_MinInt(int32_t v) { /* Returns the maximum satisfiable value for a given symbolic value, given * the constraints present on that value. */ uint32_t DeepState_MaxUInt(uint32_t v) { +#ifdef BUILD_S2E + DeepState_Abandon("MaxUInt not yet supported by S2E"); +#endif return v; } @@ -319,16 +378,24 @@ int32_t DeepState_MaxInt(int32_t v) { void _DeepState_Assume(int expr, const char *expr_str, const char *file, unsigned line) { +#ifdef BUILD_S2E + s2e_assume(expr); +#else if (!expr) { DeepState_LogFormat(DeepState_LogError, "%s(%u): Assumption %s failed", file, line, expr_str); DeepState_Abandon("Assumption failed"); } +#endif } int DeepState_IsSymbolicUInt(uint32_t x) { +#ifdef BUILD_S2E + return s2e_is_symbolic(&x, sizeof(x)); +#else (void) x; +#endif return 0; } @@ -801,6 +868,9 @@ void __stack_chk_fail(void) { #ifndef LIBFUZZER __attribute__((weak)) int main(int argc, char *argv[]) { +#ifdef BUILD_S2E + DeepState_UsingSymExec = 1; +#endif int ret = 0; DeepState_Setup(); DeepState_InitOptions(argc, argv); diff --git a/src/lib/Log.c b/src/lib/Log.c index b352df16..2492973f 100644 --- a/src/lib/Log.c +++ b/src/lib/Log.c @@ -31,6 +31,10 @@ #include "deepstate/DeepState.h" #include "deepstate/Log.h" +#ifdef BUILD_S2E +#include "s2e/s2e.h" +#endif + #undef printf #undef vprintf #undef fprintf @@ -82,7 +86,11 @@ void DeepState_Log(enum DeepState_LogLevel level, const char *str) { memset(DeepState_LogBuf, 0, DeepState_LogBufSize); snprintf(DeepState_LogBuf, DeepState_LogBufSize, "%s: %s\n", DeepState_LogLevelStr(level), str); +#ifdef BUILD_S2E + s2e_printf("[DeepState] %s", DeepState_LogBuf); +#else fputs(DeepState_LogBuf, stderr); +#endif if (DeepState_LogError == level) { DeepState_SoftFail(); diff --git a/src/lib/Stream.c b/src/lib/Stream.c index f6c15c98..c87eec68 100644 --- a/src/lib/Stream.c +++ b/src/lib/Stream.c @@ -25,6 +25,10 @@ #include "deepstate/DeepState.h" #include "deepstate/Log.h" +#ifdef BUILD_S2E +#include "s2e/s2e.h" +#endif + DEEPSTATE_BEGIN_EXTERN_C enum { @@ -159,6 +163,19 @@ static void CheckCapacity(struct DeepState_Stream *stream, DEEPSTATE_NOINLINE void _DeepState_StreamInt(enum DeepState_LogLevel level, const char *format, const char *unpack, uint64_t *val) { +#ifdef BUILD_S2E + if (s2e_is_symbolic(&level, sizeof(level))) { + DeepState_Abandon("Log level must be concrete"); + } + if (s2e_is_symbolic((void*) format, strlen(format))) { + DeepState_Abandon("Format string must be concrete"); + } + if (s2e_is_symbolic((void*) unpack, strlen(unpack))) { + DeepState_Abandon("Unpack string must be concrete"); + } + + s2e_concretize((void*) val, sizeof(*val)); +#endif struct DeepState_Stream *stream = &(DeepState_Streams[level]); int size = 0; int remaining_size = DeepState_StreamSize - stream->size; @@ -177,6 +194,19 @@ void _DeepState_StreamInt(enum DeepState_LogLevel level, const char *format, DEEPSTATE_NOINLINE void _DeepState_StreamFloat(enum DeepState_LogLevel level, const char *format, const char *unpack, double *val) { +#ifdef BUILD_S2E + if (s2e_is_symbolic(&level, sizeof(level))) { + DeepState_Abandon("Log level must be concrete"); + } + if (s2e_is_symbolic((void*) format, strlen(format))) { + DeepState_Abandon("Format string must be concrete"); + } + if (s2e_is_symbolic((void*) unpack, strlen(unpack))) { + DeepState_Abandon("Unpack string must be concrete"); + } + + s2e_concretize((void*) val, sizeof(*val)); +#endif struct DeepState_Stream *stream = &(DeepState_Streams[level]); int remaining_size = DeepState_StreamSize - stream->size; int size = snprintf(&(stream->message[stream->size]), @@ -189,6 +219,16 @@ void _DeepState_StreamFloat(enum DeepState_LogLevel level, const char *format, DEEPSTATE_NOINLINE void _DeepState_StreamString(enum DeepState_LogLevel level, const char *format, const char *str) { +#ifdef BUILD_S2E + if (s2e_is_symbolic(&level, sizeof(level))) { + DeepState_Abandon("Log level must be concrete"); + } + if (s2e_is_symbolic((void*) format, strlen(format))) { + DeepState_Abandon("Format string must be concrete"); + } + + s2e_concretize((void*) str, strlen(str)); +#endif struct DeepState_Stream *stream = &(DeepState_Streams[level]); int remaining_size = DeepState_StreamSize - stream->size; int size = snprintf(&(stream->message[stream->size]),