Commit 1437f25d authored by Olivier Nicole's avatar Olivier Nicole
Browse files

First commit

parents
.PHONY: all checknix rq0 rq3
TARGETS = "rq0 rq3 rq3_noprint rq4and5_<n>"
analysis_log = /tmp/log
all: checknix
@echo "Please specify a target to run, i.e. one of: " $(TARGETS)
checknix:
@if [ -z $(NIX_ARTIFACT_ENV) ]; then \
echo "Not in the suitable environment to run the artifact. Please open the required environment by typing 'nix-shell'."; \
exit 1; \
fi
rq0: checknix rq0_0 rq0_1 rq0_2 rq0_3 rq0_4 rq0_5 rq0_6
rq0_0:
@echo "Analyzing kernel with arbitrary user-controlled jump..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 0
rq0_1:
@echo "Analyzing kernel with code descriptor corruption..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 1
rq0_2:
@echo "Analyzing kernel with data segment corruption..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 2
rq0_3:
@echo "Analyzing kernel with arbitrary user-controlled write..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 3
rq0_4:
@echo "Analyzing kernel with arbitrary user-controlled read..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 4
rq0_5:
@echo "Analyzing kernel with illegal opcode..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 5
rq0_6:
@echo "Analyzing kernel with division by zero..."
@export analysis_log=$(analysis_log) ; \
./scripts/analyze_with_bug.sh 6
rq3: checknix
@export ntasks_args=10 \
param_or_fixed=param \
opt_flags='-O1 -O2 -O3 -Os' \
compilers='gcc clang' \
scheduling_algs='rr fp edf' \
dyn_threads_args='nodyn dyn' \
printing_args='noprint print' ; \
./scripts/all_verif.sh
rq3_noprint: checknix
@export ntasks_args=10 \
param_or_fixed=param \
opt_flags='-O1 -O2 -O3 -Os' \
compilers='gcc clang' \
scheduling_algs='rr fp edf' \
dyn_threads_args='nodyn dyn' \
printing_args='noprint' ; \
./scripts/all_verif.sh
rq4and5_%: checknix
@./scripts/rq4and5.sh $*
This describes the artifact for the article “No Crash, No Exploit: Automated
Verification of Embedded Kernels”.
This artifact should reproduce the experiments related to the following research
questions (RQs) from the article:
- RQ0 (Soundness check): Does our analyzer fail to verify APE and ARTE when the
kernel is vulnerable or buggy?
- RQ3 (Genericity): Can our method apply on different kernels, hardware
architectures and toolchains?
- RQ4 (Automation): Is it possible to prove APE and ARTE in OS kernels fully
automatically?
- RQ5 (Scalability): Can our method scale to large numbers of tasks?
Material to reproduce experiments for RQ1 and RQ2 is omitted because it depends
on proprietary executables.
# Installation
## Virtual machine
1. Download the [image](https://doi.org/10.5281/zenodo.4670548).
2. Import and start the image in a virtualization software (we tested it with
VirtualBox).
User credentials for the VM:
login: demo
password: demo
You can use `sudo` to perform privileged operations if needed.
## Using Nix
If you have Nix installed on your system, you can follow the “Usage”
instructions below directly: commands like `nix-shell` should work. Please be
aware that installing the OCaml ecosystem and compiling all the sources can take
a while (up to several dozen minutes).
# Contents of the artifact
This artifact contains:
- A copy of the source code of EducRTOS (directory `educrtos`).
- A copy of the source code of the Codex abstract interpretation library
(directory `libase`).
- A copy of the source code of BINSEC/Codex (directory `binsec`). Binsec is a
general-purpose binary analysis tool. Our verification module is in
`binsec/src/codex`.
- Scripts and other auxiliary files (directories `nix` and `scripts`).
# Usage
## Common to all experiments
IMPORTANT NOTICE: to launch any experiment, you need to navigate to the artifact
root directory (in the VM, `cd /home/demo/Desktop/rtas21_artifact`) and enter
the command `nix-shell`. This will yield a shell where our tool is available.
The tool is not installed outside of the shell yielded by `nix-shell`.
Each of the experiments (see below) implies to build various versions of EducRTOS
and attempt to verify them. Every time it happens, the artifact will print a
line similar to:
```
/home/demo/Desktop/rtas21_artifact/scripts/verif_for.sh 10 param rr clang nodyn noprint -Os
```
You may execute this command yourself to re-launch the build-and-verify
procedure and inspect the analysis log in `/tmp/log`. The log contains the
emitted alarms. Note that due to the method we use (detailed in the paper),
alarms emitted during stage "Init 0" have no consequences for the verification
of the kernel, and thus are not reported outside of the logs.
The latest built version of EducRTOS is at `educrtos/system_${n}tasks.exe`,
where `${n}` is the number of user tasks included in the image. There is also an
objdump at `educrtos/system_${n}tasks.objdump`. The inferred control flow graphs
of the kernel are in the `rtas21_artifact/cfg` directory.
## RQ0: Soundness check
Inside `nix-shell`, execute `make rq0` from the artifact root. Seven versions of
EducRTOS with purposefully injected bugs will be compiled and analyzed. The
seven verifications should fail.
## RQ3: Genericity
Inside `nix-shell`, execute `make rq3` from the artifact root. This experiment
will build and attempt to verify 96 versions of EducRTOS with varying
parameters, as described in the paper. With our hardware setup, this takes about
90 minutes. All versions should pass the verifications without alarms.
You can run `make rq3_noprint` to exclude the 48 EducRTOS versions with debug
printing enabled, which are slower to verify. With our hardware setup, this
takes about 10 minutes.
## RQ4 and RQ5: Automation and Scalability
Inside `nix-shell`, you can run `make rq4and5_n`, with `n` replaced by a
specific number of tasks. The artifact will build and verify an kernel image
bundled with n tasks, first in parameterized mode, then in in-context mode.
Only a limited set of values of n is supported, namely 1, 2, 5, 10, 50, 100,
500, 1000, 2000, 5000, 10000 and 100000. New values of n can be supported by
adding new `TASKS_${n}tasks` and `DEPS_${n}tasks` variables in
`educrtos/Makefile`.
Please be aware that for big task counts, memory consumption becomes very high
(this is an implementation issue that limits our scalability as the system swaps
for large number of tasks), as shown by Figure 8 in the paper. For task counts
greater than 1000, only the parameterized verification will be performed.
Regarding the in-context verification: you may notice that it succeeds for 1, 2
and 5 tasks, but an alarm is emitted with greater task counts. This false alarm
appears because the in-context verification fails to verify a complex invariant
on x86 segment descriptors using only numeric information. Parameterized
verification, on the contrary, succeeds independently of the number of tasks.
This supports our statement that "Fully-automated in-context verification with no
annotation is achievable on very simple kernels, but is not robust enough for
more complex kernels."
# Modifying EducRTOS
In order to modify parts of EducRTOS, you need to navigate to the `educrtos`
directory, and run:
```
nix-shell --arg clang true
```
to compile with clang, and
```
nix-shell --arg clang false
```
to compile with GCC. Then you should run `make system_${n}tasks.exe` to build,
where `${n}` is the number of tasks to include in the executable (with the same
restrictions as in RQ4&5). It will build a version of EducRTOS with
earliest-deadline-first scheduling, dynamic task creation and printing
activated, using the `-O1` flag.
You can also test the OS in QEMU by running `make system_${n}tasks.qemu`.
Finally, you can attempt to verify the modified OS by running e.g.:
```
$ARTIFACT_ROOT/scripts/verif_for.sh 10 param rr gcc nodyn noprint -O1
```
# Modifying the analyzer
If you modify the sources of the analyzer, either in `binsec` or in `libase`, in
order to recompile it, you need to exit any `nix-shell` you were in, and then
run `nix-shell` again in the artifact root directory
(in the VM, `/home/demo/Desktop/rtas21_artifact`).
The definition of the "stack" of abstract domains used in the
analysis is defined in file `binsec/src/codex/dba2Codex.ml` and can be modified.
For instance, the following change:
```diff
diff --git a/src/codex/dba2Codex.ml b/src/codex/dba2Codex.ml
index 96abfc8a1..188ba2371 100644
--- a/src/codex/dba2Codex.ml
+++ b/src/codex/dba2Codex.ml
@@ -113,7 +113,7 @@ module Create () : Sig = struct
module Propag_domain = Domains_constraints_constraint_propagation.Make
(Constraints)(Ival_with_sentinel_basis)
module Scalar0 = Constraint_domain2.Make(Constraints)(Propag_domain)
- module Scalar = Bitwise_domain.Make (Scalar0)
+ module Scalar = (* Bitwise_domain.Make *) (Scalar0)
module Region_numeric = Region_numeric_offset.Make(Scalar)
module Numeric : Codex.Memory_sig.Operable_Value_Whole
```
leaves out the `Bitwise_domain` from the analysis, which will make the analyzer
emit false alarms due to imprecisions on the accessible range of the loaded x86
segment.
# Tests
BINSEC/Codex relies on two components that are tested independently.
We rely mainly on the ELF loader and instruction decoder of BINSEC, which have
been used in a large number of publications. The IR decoding of BINSEC is tested
by comparing the results of the BINSEC interpreter and symbolic execution engine
against real executions.
The Codex abstract interpretation library is mainly tested on C code, using a
collection of unit (C) tests, and comparison with other analyzers (such as
Frama-C's Eva) on large benchmarks. These C-based tests depend on Frama-C, that
we did not include in the artifact VM (as the purpose of the artifact is to
analyze binary code).
BINSEC/Codex itself is tested for soundness using our soundness check (RQ0) and
our collection of 96 EducRTOS versions (RQ4).
*.cmi
*.cmti
*.conflicts
/src/_build/*
*.o
*.info
*.objdump
*.annot
*.cmt
*.dir-locals.el
/.projectile
*.piqi
*.dba
*.dot
*.opc
*.trace
*.cmo
autom4te*
/src/test_runner
/src/oUnit-*.log
/src/oUnit-*.cache
/src/parser/lexer_infos.ml
/src/parser/parser.ml
/src/parser/parser.mli
/src/parser/parser_infos.ml
/src/parser/parser_infos.mli
/src/parser/policy_parser.ml
/src/parser/policy_parser.mli
/src/parser/policy_token.ml
*.cmx
/tests/simulation/test_runner
/src/smtutils/smtlib_lexer.ml
/src/smtutils/smtlib_parser.ml
/src/smtutils/smtlib_parser.mli
/config.status
/config.log
*.pb.cc
*.pb.h
/Config.mk
cfg_dba.pdf
cfg_opcode.pdf
/configure
/.depend
apiref
/www/htdocs/distrib/binsec.tgz
plateforme/*.tgz
/src/binsec.docdir
/pinsec/build/
/src/config.ml
/src/binsec*
/src/piqi
/src/.depend
/src/main.native
/src/parser/SMTLexerWp.ml
/src/parser/SMTParserWp.ml
/src/parser/SMTParserWp.mli
/src/parser/dbacsl_parser.ml
/src/parser/dbacsl_parser.mli
/src/parser/dbacsl_token.ml
/src/parser/lexer.ml
/src/smtlib/smtlib_lexer.ml
/src/smtlib/smtlib_parser.ml
/src/smtlib/smtlib_parser.mli
# Vim
.*.swp
# macOS
.DS_Store
.AppleDouble
.LSOverride
.DocumentRevisions-V100
.fseventsd
.Spotlight-V100
.TemporaryItems
.Trashes
.VolumeIcon.icns
.com.apple.timemachine.donotpresent
.AppleDB
.AppleDesktop
Network Trash Folder
Temporary Items
.apdisk
/src/kernel/config.ml
/src/kernel/config.mli
* 0.3
** Features
- New architecture support : RISC-V 32 bits
- Support for DWARF-4 debug instruction format
- Support to import IDA control-flow graph
- Add documented plugin creation example : mnemonic count [mcount]
- New Makefile 'library' to ease plugin creation
** Fixes
- Fix (vectorized instructions) x86 decoder
** Misc
- Detach PINSEC to own repository (support to be deprecated in later version)
* 0.2 [2018-10-01 Mon]
- New symbolic execution engine
- New interpreter for binary code
- Improved logical representation for formulas
- New internal control-flow-graph representation
- Directive language for symbolic execution control
- Support for new PIN tool xtrasec
- Improved x86 decoder
- Fixed bugs reported by KAIST
- Docker support
- includes Unisim-vp ARM v7 decoder
- includes new PIN tool xtrasec
* 0.1 [2017-03-01 Wed]
First release
##########################################################################
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2019 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
.PHONY: default all bin byt clean cleandir configure depend beforedepend
# Compilation rules
.SUFFIXES: .o .c
.SUFFIXES: .cmx .cmxa .cmo .cmi .cma .ml .mli .mll .mly
.cmo.o:
$(PP) "COBJ $@"
$(CAMLBYT) -custom -output-obj -o $@ $<
.c.o:
$(CAMLBYT) -ccopt "-fPIC -o $@" -c $<
.ml.cmo:
$(PP_BYT) $@
$(CAMLBYT) $(CAMLINCLUDES) $(CAMLFLAGS) $(CAMLWARNINGS) -c $<
.mli.cmi:
$(PP_BYT) $@
$(CAMLBYT) $(CAMLFLAGS) $(CAMLINCLUDES) -c $<
.ml.cmx:
$(PP_OPT) $@
$(CAMLBIN) $(CAMLINCLUDES) $(CAMLFLAGS) $(CAMLWARNINGS) -c $<
.mly.ml:
$(PP_YACC) $@
$(CAMLYAC) $(CAMLYACOPTS) $<
.mly.mli:
$(PP_YACC) $@
$(CAMLYAC) $(CAMLYACOPTS) $<
.mll.ml:
$(PP_LEX) $@
$(CAMLLEX) $(CAMLLEXOPTS) $<
# Generic clean up
cleandir::
$(RRM) *.cm[ioxa] *.cmxa *.o *.a *.annot *.obj *.lib *~ .*~ a.out .\#*
configure:: cleandir
# Rebuilding dependencies
depend:: beforedepend
$(CAMLDEP) $(CAMLINCLUDES) $(CAMLFILES) > .depend
include .depend
##########################################################################
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2019 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
CAMLC ?=@OCAMLC@
CAMLOPT ?=@OCAMLOPT@
CAMLLEX ?=@OCAMLLEX@
CAMLLEXOPTS ?=
CAMLYAC ?=@MENHIR@
CAMLYACOPTS ?=
CAMLDEP ?=@OCAMLDEP@
# Rationale for warning exclusions:
# - 42 is only valid in OCaml < 4.00
# - 4 fragile pattern matching is authorized (can be hard to remove on big ASTs)
# - 3 deprecated feature are ok (sometimes you have a newer compiler than older supported version)
CAMLWARNINGS ?=-w +a-4-3-42
CAMLFLAGS ?=-g -bin-annot
CAMLDOC ?=@OCAMLDOC@
CAMLFIND ?=@OCAMLFIND@
BEST ?=@OCAMLBEST@
OCAMLBUILD?=@OCAMLBUILD@
# By default, ocamlbuild will NOT be used, unless the environment variable
# USE_OCAMLBUILD is set to something else than "no".
USE_OCAMLBUILD ?= no
OCB_OPTIONS ?=-use-ocamlfind -I .
PIQI ?=@PIQI@
PIQI_FLAGS ?= of-proto -I $(PROTO_DIR)
PIQI_DIR ?=@PIQI_DIR@
PROTOC ?=@PROTOC@
PROTOC_FLAGS ?= --proto_path=$(BINSEC_DIR)/$(PROTO_DIR) --cpp_out=$(CPP_PROTOBUF_DIR)
PIQI2CAML ?=@PIQI2CAML@
PIQI2CAML_FLAGS ?= --multi-format -C $(PIQI_DIR)
DESTDIR ?=
prefix ?=@prefix@
exec_prefix ?=@exec_prefix@
datarootdir ?=@datarootdir@
datadir ?=@datadir@
BINDIR ?="$(DESTDIR)@bindir@"
LIBDIR ?="$(DESTDIR)@libdir@"
DATADIR ?="$(DESTDIR)@datarootdir@"
MANDIR ?="$(DESTDIR)@mandir@"
VERBOSEMAKE?=no
ifneq ($(VERBOSEMAKE),no) # Do not change to ifeq ($(VERBOSEMAKE),yes), as this
# version makes it easier for the user to set the
# option on the command-line to investigate
# Makefile-related problems
# ignore the PRINT_* materials but print all the other commands
PP = @true
# prevent the warning "jobserver unavailable: using -j1".
# see GNU make manual (section 5.7.1 and appendix B)
QUIET_MAKE:= + $(MAKE)
# prevent the warning: "-jN forced in submake: disabling jobserver mode".
# see GNU make manual (appendix B)
MAKE := MAKEFLAGS="$(patsubst j,,$(MAKEFLAGS))" $(MAKE)
else
# print the PP_* materials
PP = @echo
# but silently execute all the other commands
# fixed bug #637: do not write spaces between flags
OLDFLAGS:=r$(MAKEFLAGS)
MAKEFLAGS:=rs$(MAKEFLAGS)
# do not silently execute other makefiles (e.g the one of why):
# the redefinition of MAKE below is for this purpose
# but use QUIET_MAKE in order to call silently the initial Makefile
QUIET_MAKE:= $(MAKE)
MAKE := MAKEFLAGS="$(OLDFLAGS)" $(MAKE)
endif
PP_BYT = $(PP) 'BYT '
PP_OPT = $(PP) 'BIN '
PP_YACC = $(PP) 'MENHIR '
PP_LEX = $(PP) 'LEX '
RM ?= rm -rf
RRM ?= rm -rf
CP ?= cp -R
MKDIR_P ?= @MKDIR_P@
CD ?= cd
TAR ?= tar cvzf
INSTALL ?= @INSTALL@
AWK ?= @AWK@
HEADACHE=@HEADACHE@
HEADACHE_CONFIG?=headers/headache_config.txt
DOT2SVG = dot -Tsvg
%.svg : %.dot
$(DOT2SVG) -o $@ $<
default: alldoc
include Makefile
# The file src/Targets.mk below is located in another directory and includes
# another file located in the same directory using relative path
# (i.e, by using include Lib.mk).
#
# Therefore for the targets of Distrib.mk to work, one needs to include the src
# directory as follows, for example when runnnig the tarball target :
#
# make -I src -f Distrib.mk tarball
#
include src/Targets.mk
# Headers & License
LICENSE_CEA_IMAG = \
$(BINSEC_LICENSE_CEA_IMAG:%=$(BINSEC_DIR)/%)
LICENSE_IMAG = \
$(BINSEC_LICENSE_IMAG:%=$(BINSEC_DIR)/%)
LICENSE_CEA = \
$(SRC_BUILD_FILES) \
$(BINSEC_LICENSE_CEA:%=$(BINSEC_DIR)/%)
LICENSE_EXTERNAL_CHLIPALA = $(BINSEC_LICENSE_EXTERNAL_CHLIPALA:%=$(BINSEC_DIR)/%)
LICENSE_EXTERNAL = $(BINSEC_EXTERNAL)
define mk_license
$(PP) $(1)
for f in $(1); do \
$(HEADACHE) -r -c $(HEADACHE_CONFIG) -h $(2) $$f; \
done
endef
.PHONY: headers
ifneq ($(HEADACHE), no)
headers:
$(call mk_license, $(LICENSE_IMAG), headers/IMAG_LGPL)
$(call mk_license, $(LICENSE_CEA_IMAG), headers/CEA_IMAG_LGPL)
$(call mk_license, $(LICENSE_CEA), headers/CEA_LGPL)
$(call mk_license, $(LICENSE_EXTERNAL_CHLIPALA), headers/BSD_CHLIPALA)
endif
DATE=$(shell date +"%Y%m%d")
RELEASE_CODE_NAME = "Astute_Asterix"
VERSION=$(shell cat VERSION)
NAME = binsec-$(VERSION)-$(DATE)
SYMLINK = $(NAME)
BINSEC_FILES = $(BINSEC_DISTRIB_FILES:%=$(SYMLINK)/$(BINSEC_DIR)/%)
SRC_BUILD_FILES = configure configure.ac \
Piqi.mk Caml.mk Config.mk.in Makefile \
install-sh CHANGES VERSION
SRC_OTHER_FILES = LICENSE README
OPAM_DIR = opam
DISTRIB_FILES = \
$(SRC_BUILD_FILES:%=$(SYMLINK)/%) \
$(SRC_OTHER_FILES:%=$(SYMLINK)/%) \
$(BINSEC_FILES) \
$(SYMLINK)/$(OPAM_DIR)
TARBALL = $(NAME).tgz
tarball: clean-tarball
autoconf
$(PP) "Making tarball $(TARBALL)"
$(PP) "Remove and relink $(SYMLINK)"
-$(RM) $(SYMLINK)
ln -sf . $(SYMLINK)
@$(TAR) $(TARBALL) $(DISTRIB_FILES)
unlink $(SYMLINK)