Commit 15841241 authored by Richard Bonichon's avatar Richard Bonichon
Browse files

Release BINSEC 0.2beta

parent 0a2dbc2e
* 0.2 [2018-07-23 Mon]
- New symbolic execution engine
- New interpreter for binary code
- Improved logical representation for formulas
- New internal control-flow-graph representation
- Action language for symbolic execution goals
- Improved x86 decoder
- Fixed bugs reported by KAIST
- Docker support
- includes Unisim-vp ARM v7 decoder
* 0.1 [2017-03-01 Wed]
First release
##########################################################################
# This file is part of Binsec. #
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2017 #
# Copyright (C) 2016-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......
##########################################################################
# This file is part of Binsec. #
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2017 #
# Copyright (C) 2016-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -22,21 +22,28 @@
CAMLC ?=@OCAMLC@
CAMLOPT ?=@OCAMLOPT@
CAMLLEX ?=@OCAMLLEX@
CAMLLEXOPTS? ?=
CAMLLEXOPTS ?=
CAMLYAC ?=@MENHIR@
CAMLYACOPTS ?=
CAMLDEP ?=@OCAMLDEP@
CAMLWARNINGS? ?=-w +a-4-3
CAMLFLAGS? ?=-g -annot
CAMLWARNINGS ?=-w +a-4-3-18
CAMLFLAGS ?=-g -bin-annot
CAMLDOC ?=@OCAMLDOC@
CAMLFIND ?=@OCAMLFIND@
BEST ?=@OCAMLBEST@
OCAMLBUILD?=@OCAMLBUILD@
OCB_OPTIONS?=-use-ocamlfind -no-hygiene -libs str,bigarray -I .
# 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)
......@@ -89,11 +96,13 @@ PP_LEX = $(PP) 'LEX '
RM ?= rm -rf
RRM ?= rm -rf
CP ?= cp -r
MKDIR ?= mkdir -p
CP ?= cp -R
MKDIR_P ?= @MKDIR_P@
CD ?= cd
TAR ?= tar cvzf
INSTALL ?= install
INSTALL ?= @INSTALL@
AWK ?= @AWK@
HEADACHE=@HEADACHE@
HEADACHE_CONFIG?=headers/headache_config.txt
......
##########################################################################
# This file is part of Binsec. #
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2017 #
# Copyright (C) 2016-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -32,7 +32,7 @@ PINSEC_BUILD_DIR = $(PINSEC_DIR)/build
CMAKE = cmake
PIN_ROOT_DIR ?= pin-2.14-71313-gcc.4.4.7-linux
pinsec: protoc
$(MKDIR) $(PINSEC_BUILD_DIR)
$(MKDIR_P) $(PINSEC_BUILD_DIR)
$(PP) "Using PIN from $(PIN_ROOT_DIR)"
($(CD) $(PINSEC_BUILD_DIR); \
$(CMAKE) -DPIN_ROOT_DIR=$(PIN_ROOT_DIR) ..)
......@@ -45,7 +45,10 @@ pinsec-clean:
BINSEC_DIR = src
binsec:
$(MAKE) -C $(BINSEC_DIR)
ifeq ($(USE_OCAMLBUILD), no)
$(MAKE) -C $(BINSEC_DIR) depend
endif
$(MAKE) -C $(BINSEC_DIR) -j
binsec-clean:
$(MAKE) -C $(BINSEC_DIR) clean
......@@ -62,6 +65,8 @@ veryclean: clean clean-configure
tests:
$(MAKE) -C tests
install:
$(MAKE) -C src install
include $(PINSEC_DIR)/Targets.mk
include $(BINSEC_DIR)/Targets.mk
##########################################################################
# This file is part of Binsec. #
# This file is part of BINSEC. #
# #
# Copyright (C) 2016-2017 #
# Copyright (C) 2016-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -25,6 +25,7 @@
$(PP) 'PIQIML $@'
$(PIQI2CAML) $(PIQI2CAML_FLAGS) $<
# $(PIQI_DIR) is created by configure script
$(PIQI_DIR)/%.piqi: $(PROTO_DIR)/%.proto
$(PP) 'PIQI $@'
$(PIQI) $(PIQI_FLAGS) -o $@ $<
......@@ -34,7 +35,7 @@ CPP_PROTOBUF_DIR = $(PINSEC_DIR)/$(PINSEC_TYPES_DIR)/protobuf
.PHONY: pre-protoc
pre-protoc:
$(MKDIR) $(CPP_PROTOBUF_DIR)
$(MKDIR_P) $(CPP_PROTOBUF_DIR)
%.pb.cc: src/proto/%.proto
$(PP) 'PROTOC $@'
......@@ -52,10 +53,7 @@ protoc: pre-protoc $(PROTO_LSRC_FILES)
clean::
$(RRM) $(CPP_PROTOBUF_DIR)
.PHONY: prepiqi
prepiqi:
$(MKDIR) $(PIQI_DIR)
$(PIQI_ML_FILES): $(PIQI_FILES)
$(PIQI_FILES): prepiqi
$(PIQI_ML_FILES) : $(PIQI_FILES)
piqi-ml : $(PIQI_ML_FILES)
# Compilation #
## BINSEC
## BINSEC
The following usual steps should do the trick:
```
% autoconf
% ./configure
% make binsec
% make install
```
To install `BINSEC`, do `cd src; make install`.
## PINSEC
......@@ -23,38 +24,11 @@ Then, go to the directory pinsec/build, and configure your build.
The build needs `CMake`.
# Use
## BINSEC
In the `src` directory.
- List of available commands:
./binsec --help
- Help about a specific command:
./binsec COMMAND --help
### Simple examples ###
# Help
```
binsec --help
```
- Linear (objdump-like) disassembly of text section
```
./binsec disasm -sections .text -dmode linear BINARY_FILE
```
- Recursive disassembly of text section
```
./binsec disasm -sections .text -dmode rec BINARY_FILE
```
- Simulation:
```
./binsec simulate -entrypoint INIT_ADDR BINARY_FILE
```
# binsec
BINSEC binary-level open-source platform
This Github repository will be the new home for news and releases of the BINSEC binary code analysis platform.
For now it is still http://binsec.gforge.inria.fr/.
We are moving in very soon. Keep in touch!
--
The BINSEC team
0.2beta
\ No newline at end of file
......@@ -583,7 +583,15 @@ PACKAGE_URL=
ac_subst_vars='LTLIBOBJS
LIBOBJS
INSTALL
PIQI_DIR
OCAMLBEST
OCB_OPTIONS
INSTALL_DATA
INSTALL_SCRIPT
INSTALL_PROGRAM
MKDIR_P
AWK
BOOLECTOR
YICES
CVC4
......@@ -598,7 +606,6 @@ PIQI
MENHIR
OCAMLLEX
OCAMLDEP
OCB_OPTIONS
OCAMLBUILD
OCAMLOPTDOTOPT
OCAMLOPT
......@@ -1685,14 +1692,14 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu
has_or_die ()
{
if test "$1" = no; then
if test x"$1" = xno; then
as_fn_error $? "$2" "$LINENO" 5
fi
}
has_lib_or_die ()
{
if test "$1" = ""; then
if test x"$1" = "x"; then
as_fn_error $? "$2" "$LINENO" 5
fi
}
......@@ -1735,6 +1742,7 @@ $as_echo "no" >&6; }
fi
has_or_die $MAKE "Could not find GNU make"
# Extract the first word of "ocamlfind", so it can be a program name with args.
set dummy ocamlfind; ac_word=$2
......@@ -1815,7 +1823,7 @@ $as_echo "no" >&6; }
fi
if test "$OCAMLC" = no; then
if test x"$OCAMLC" = xno; then
as_fn_error $? "\"Could not find ocamlc.\"" "$LINENO" 5
else
# Extract the first word of "ocamlc.opt", so it can be a program name with args.
......@@ -1865,12 +1873,13 @@ fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking version of OCaml" >&5
$as_echo_n "checking version of OCaml... " >&6; }
OCAMLCVERSION=`$OCAMLC -version`
LEAST_VERSION="4.02.1"
LEAST_VERSION="4.04.2"
MOST_VERSION="4.05.0"
case $OCAMLCVERSION in
4.02*) $as_echo "Good! ($OCAMLCVERSION)";;
4.03*) $as_echo "Good! ($OCAMLCVERSION)";;
4.04*) $as_echo "Good! ($OCAMLCVERSION)";;
*) as_fn_error $? "\"Please use at least $LEAST_VERSION (found $OCAMLCVERSION).\"" "$LINENO" 5;;
4.05*) $as_echo "Good! ($OCAMLCVERSION)";;
# no support for 4.06.* && 4.07 due to piqilib dependency on optcomp which depends on ocaml < 4.06.0
*) as_fn_error $? "\"Please use an ocaml version >= $LEAST_VERSION and <= $MOST_VERSION (found $OCAMLCVERSION).\"" "$LINENO" 5;;
esac
......@@ -2005,13 +2014,13 @@ $as_echo "no" >&6; }
fi
has_or_die $OCAMLBUILD "Could not find ocamlbuild"
OCB_OPTIONS="-use-ocamlfind -no-hygiene -lflags ../loader_ml.o -libs nums,str -I ."
if test "$OCAMLBUILD" == "no"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"Could not find ocamlbuild -- you will only be able to build BINSEC through make\"" >&5
$as_echo "$as_me: WARNING: \"Could not find ocamlbuild -- you will only be able to build BINSEC through make\"" >&2;}
fi
OCB_OPTIONS="-use-ocamlfind -I ."
# ocamldep
# Extract the first word of "ocamldep", so it can be a program name with args.
......@@ -2054,7 +2063,7 @@ fi
has_or_die $OCAMLDEP "Could not find ocamldep"
OCAMLDEPVERSION=`ocamldep -version | sed -e 's/ocamldep, version \(.*\)/\1/'`
if test "$OCAMLDEPVERSION" != "$OCAMLCVERSION"; then
if test x"$OCAMLDEPVERSION" != x"$OCAMLCVERSION"; then
as_fn_error $? "\"ocamldep version $OCAMLCVERSION conflicts with ocamlc version $OCAMLCVERSION. Should be the same.\"" "$LINENO" 5
fi
......@@ -2165,31 +2174,31 @@ $as_echo "$MYLIBPATH" >&6; }
check_lib "ocamlgraph"
OCAMLGRAPH=$MYLIBPATH
if test "$LIB_FOUND" = "no"; then
if test x"$LIB_FOUND" = x"no"; then
as_fn_error $? "\"ocamlgraph not found\"" "$LINENO" 5
fi
check_lib "piqilib"
PIQILIB=$MYLIBPATH
if test "$LIB_FOUND" = "no"; then
if test x"$LIB_FOUND" = x"no"; then
as_fn_error $? "\"piqilib not found\"" "$LINENO" 5
fi
check_lib "zarith"
ZARITH=$MYLIBPATH
if test "$LIB_FOUND" = "no"; then
if test x"$LIB_FOUND" = x"no"; then
as_fn_error $? "\"zarith not found\"" "$LINENO" 5
fi
check_lib "ZMQ"
check_lib "zmq"
ZMQ=$MYLIBPATH
if test "$LIB_FOUND" = "no"; then
if test x"$LIB_FOUND" = x"no"; then
as_fn_error $? "\"zmq not found\"" "$LINENO" 5
fi
check_lib "llvm"
LLVM=$MYLIBPATH
if test "$LIB_FOUND" = "no"; then
if test x"$LIB_FOUND" = x"no"; then
as_fn_error $? "\"llvm not found\"" "$LINENO" 5
fi
......@@ -2357,7 +2366,7 @@ $as_echo "no" >&6; }
fi
if test "$OCAMLDOC" = no; then
if test x"$OCAMLDOC" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"Documentation generation disabled.\"" >&5
$as_echo "$as_me: WARNING: \"Documentation generation disabled.\"" >&2;}
else
......@@ -2403,7 +2412,7 @@ $as_echo "no" >&6; }
fi
if test "$CMAKE" = no; then
if test x"$CMAKE" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"You will not be able to compile PINSEC\"" >&5
$as_echo "$as_me: WARNING: \"You will not be able to compile PINSEC\"" >&2;}
fi
......@@ -2447,7 +2456,7 @@ $as_echo "no" >&6; }
fi
if test "$HEADACHE" = no; then
if test x"$HEADACHE" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"License generation disabled.\"" >&5
$as_echo "$as_me: WARNING: \"License generation disabled.\"" >&2;}
fi
......@@ -2490,7 +2499,7 @@ $as_echo "no" >&6; }
fi
if test "$DOT" = no; then
if test x"$DOT" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"dot not found: disabling documentation generation.\"" >&5
$as_echo "$as_me: WARNING: \"dot not found: disabling documentation generation.\"" >&2;}
fi
......@@ -2534,7 +2543,7 @@ $as_echo "no" >&6; }
fi
if test "$Z3" = no; then
if test x"$Z3" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"z3 not found: some parts of binsec might not work.\"" >&5
$as_echo "$as_me: WARNING: \"z3 not found: some parts of binsec might not work.\"" >&2;}
fi
......@@ -2577,7 +2586,7 @@ $as_echo "no" >&6; }
fi
if test "$CVC4" = no; then
if test x"$CVC4" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"cvc4 not found: some parts of binsec might not work.\"" >&5
$as_echo "$as_me: WARNING: \"cvc4 not found: some parts of binsec might not work.\"" >&2;}
fi
......@@ -2620,7 +2629,7 @@ $as_echo "no" >&6; }
fi
if test "$YICES" = no; then
if test x"$YICES" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"yices-smt2 not found: some parts of binsec might not work.\"" >&5
$as_echo "$as_me: WARNING: \"yices-smt2 not found: some parts of binsec might not work.\"" >&2;}
fi
......@@ -2663,11 +2672,225 @@ $as_echo "no" >&6; }
fi
if test "$BOOLECTOR" = no; then
if test x"$BOOLECTOR" = xno; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: \"boolector not found: some parts of binsec might not work.\"" >&5
$as_echo "$as_me: WARNING: \"boolector not found: some parts of binsec might not work.\"" >&2;}
fi
ac_config_commands="$ac_config_commands depend"
PIQI_DIR="piqi"
ac_config_commands="$ac_config_commands piqi_directory"
# See https://www.gnu.org/software/autoconf/manual/autoconf-2.69/html_node/Particular-Programs.html
for ac_prog in gawk mawk nawk awk
do
# Extract the first word of "$ac_prog", so it can be a program name with args.
set dummy $ac_prog; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_AWK+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$AWK"; then
ac_cv_prog_AWK="$AWK" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_AWK="$ac_prog"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
AWK=$ac_cv_prog_AWK
if test -n "$AWK"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $AWK" >&5
$as_echo "$AWK" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
test -n "$AWK" && break
done
ac_aux_dir=
for ac_dir in "$srcdir" "$srcdir/.." "$srcdir/../.."; do
if test -f "$ac_dir/install-sh"; then
ac_aux_dir=$ac_dir
ac_install_sh="$ac_aux_dir/install-sh -c"
break
elif test -f "$ac_dir/install.sh"; then
ac_aux_dir=$ac_dir
ac_install_sh="$ac_aux_dir/install.sh -c"
break
elif test -f "$ac_dir/shtool"; then
ac_aux_dir=$ac_dir
ac_install_sh="$ac_aux_dir/shtool install -c"
break
fi
done
if test -z "$ac_aux_dir"; then
as_fn_error $? "cannot find install-sh, install.sh, or shtool in \"$srcdir\" \"$srcdir/..\" \"$srcdir/../..\"" "$LINENO" 5
fi
# These three variables are undocumented and unsupported,
# and are intended to be withdrawn in a future Autoconf release.
# They can cause serious problems if a builder's source tree is in a directory
# whose full name contains unusual characters.
ac_config_guess="$SHELL $ac_aux_dir/config.guess" # Please don't use this var.
ac_config_sub="$SHELL $ac_aux_dir/config.sub" # Please don't use this var.
ac_configure="$SHELL $ac_aux_dir/configure" # Please don't use this var.
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for a thread-safe mkdir -p" >&5
$as_echo_n "checking for a thread-safe mkdir -p... " >&6; }
if test -z "$MKDIR_P"; then
if ${ac_cv_path_mkdir+:} false; then :
$as_echo_n "(cached) " >&6
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH$PATH_SEPARATOR/opt/sfw/bin
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_prog in mkdir gmkdir; do
for ac_exec_ext in '' $ac_executable_extensions; do
as_fn_executable_p "$as_dir/$ac_prog$ac_exec_ext" || continue
case `"$as_dir/$ac_prog$ac_exec_ext" --version 2>&1` in #(
'mkdir (GNU coreutils) '* | \
'mkdir (coreutils) '* | \
'mkdir (fileutils) '4.1*)
ac_cv_path_mkdir=$as_dir/$ac_prog$ac_exec_ext
break 3;;
esac
done
done
done
IFS=$as_save_IFS
fi
test -d ./--version && rmdir ./--version
if test "${ac_cv_path_mkdir+set}" = set; then
MKDIR_P="$ac_cv_path_mkdir -p"
else
# As a last resort, use the slow shell script. Don't cache a
# value for MKDIR_P within a source directory, because that will
# break other packages using the cache if that directory is
# removed, or if the value is a relative name.
MKDIR_P="$ac_install_sh -d"
fi
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $MKDIR_P" >&5
$as_echo "$MKDIR_P" >&6; }
# Find a good install program. We prefer a C program (faster),
# so one script is as good as another. But avoid the broken or
# incompatible versions:
# SysV /etc/install, /usr/sbin/install
# SunOS /usr/etc/install
# IRIX /sbin/install
# AIX /bin/install
# AmigaOS /C/install, which installs bootblocks on floppy discs
# AIX 4 /usr/bin/installbsd, which doesn't work without a -g flag
# AFS /usr/afsws/bin/install, which mishandles nonexistent args
# SVR4 /usr/ucb/install, which tries to use the nonexistent group "staff"
# OS/2's system install, which has a completely different semantic
# ./install, which can be erroneously created by make from ./install.sh.
# Reject install programs that cannot install multiple files.
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for a BSD-compatible install" >&5
$as_echo_n "checking for a BSD-compatible install... " >&6; }
if test -z "$INSTALL"; then
if ${ac_cv_path_install+:} false; then :
$as_echo_n "(cached) " >&6
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
# Account for people who put trailing slashes in PATH elements.
case $as_dir/ in #((
./ | .// | /[cC]/* | \
/etc/* | /usr/sbin/* | /usr/etc/* | /sbin/* | /usr/afsws/bin/* | \
?:[\\/]os2[\\/]install[\\/]* | ?:[\\/]OS2[\\/]INSTALL[\\/]* | \
/usr/ucb/* ) ;;
*)
# OSF1 and SCO ODT 3.0 have their own names for install.
# Don't use installbsd from OSF since it installs stuff as root
# by default.
for ac_prog in ginstall scoinst install; do
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_prog$ac_exec_ext"; then
if test $ac_prog = install &&
grep dspmsg "$as_dir/$ac_prog$ac_exec_ext" >/dev/null 2>&1; then
# AIX install. It has an incompatible calling convention.
:
elif test $ac_prog = install &&
grep pwplus "$as_dir/$ac_prog$ac_exec_ext" >/dev/null 2>&1; then
# program-specific install script used by HP pwplus--don't use.
:
else
rm -rf conftest.one conftest.two conftest.dir
echo one > conftest.one
echo two > conftest.two
mkdir conftest.dir
if "$as_dir/$ac_prog$ac_exec_ext" -c conftest.one conftest.two "`pwd`/conftest.dir" &&
test -s conftest.one && test -s conftest.two &&
test -s conftest.dir/conftest.one &&
test -s conftest.dir/conftest.two
then
ac_cv_path_install="$as_dir/$ac_prog$ac_exec_ext -c"
break 3
fi
fi
fi
done
done
;;
esac
done
IFS=$as_save_IFS
rm -rf conftest.one conftest.two conftest.dir