Commit ff550b05 authored by Frédéric Recoules's avatar Frédéric Recoules
Browse files

Release BINSEC 0.4.0

parent f9a22ba6
# Created by https://www.toptal.com/developers/gitignore/api/ocaml,c,c++,python,vim,emacs,macos
# Edit at https://www.toptal.com/developers/gitignore?templates=ocaml,c,c++,python,vim,emacs,macos
### C ###
# Prerequisites
*.d
# Object files
*.o
*.ko
*.obj
*.elf
# Linker output
*.ilk
*.map
*.exp
# Precompiled Headers
*.gch
*.pch
# Libraries
*.lib
*.a
*.la
*.lo
# Shared objects (inc. Windows DLLs)
*.dll
*.so
*.so.*
*.dylib
# Executables
*.exe
*.out
*.app
*.i*86
*.x86_64
*.hex
# Debug files
*.dSYM/
*.su
*.idb
*.pdb
# Kernel Module Compile Results
*.mod*
*.cmd
.tmp_versions/
modules.order
Module.symvers
Mkfile.old
dkms.conf
### C++ ###
# Prerequisites
# Compiled Object files
*.slo
# Precompiled Headers
# Compiled Dynamic libraries
# Fortran module files
*.mod
*.smod
# Compiled Static libraries
*.lai
# Executables
### Emacs ###
# -*- mode: gitignore; -*-
*~
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
# Org-mode
.org-id-locations
*_archive
# flymake-mode
*_flymake.*
# eshell files
/eshell/history
/eshell/lastdir
# elpa packages
/elpa/
# reftex files
*.rel
# AUCTeX auto folder
/auto/
# cask packages
.cask/
dist/
# Flycheck
flycheck_*.el
# server auth directory
/server/
# projectiles files
.projectile
# directory configuration
.dir-locals.el
# network security
/network-security.data
### macOS ###
# General
.DS_Store
.AppleDouble
.LSOverride
# Icon must end with two \r
Icon
# Thumbnails
._*
# Files that might appear in the root of a volume
.DocumentRevisions-V100
.fseventsd
.Spotlight-V100
.TemporaryItems
.Trashes
.VolumeIcon.icns
.com.apple.timemachine.donotpresent
# Directories potentially created on remote AFP share
.AppleDB
.AppleDesktop
Network Trash Folder
Temporary Items
.apdisk
### OCaml ###
*.annot
*.cmo
*.cma
*.cmi
*.cmx
*.cmxs
*.cmxa
# ocamlbuild working directory
_build/
# ocamlbuild targets
*.byte
*.native
# oasis generated files
setup.data
setup.log
# Merlin configuring file for Vim and Emacs
.merlin
# Dune generated files
*.install
# Local OPAM switch
_opam/
### Python ###
# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class
# C extensions
# Distribution / packaging
.Python
build/
develop-eggs/
downloads/
eggs/
.eggs/
lib/
lib64/
parts/
sdist/
var/
wheels/
share/python-wheels/
*.egg-info/
.installed.cfg
*.egg
MANIFEST
# PyInstaller
# Usually these files are written by a python script from a template
# before PyInstaller builds the exe, so as to inject date/other infos into it.
*.manifest
*.spec
# Installer logs
pip-log.txt
pip-delete-this-directory.txt
# Unit test / coverage reports
htmlcov/
.tox/
.nox/
.coverage
.coverage.*
.cache
nosetests.xml
coverage.xml
*.cover
*.py,cover
.hypothesis/
.pytest_cache/
cover/
# Translations
*.mo
*.pot
# Django stuff:
*.log
local_settings.py
db.sqlite3
db.sqlite3-journal
# Flask stuff:
instance/
.webassets-cache
# Scrapy stuff:
.scrapy
# Sphinx documentation
docs/_build/
# PyBuilder
.pybuilder/
target/
# Jupyter Notebook
.ipynb_checkpoints
# IPython
profile_default/
ipython_config.py
# pyenv
# For a library or package, you might want to ignore these files since the code is
# intended to run in multiple environments; otherwise, check them in:
# .python-version
# pipenv
# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
# However, in case of collaboration, if having platform-specific dependencies or dependencies
# having no cross-platform support, pipenv may install dependencies that don't work, or not
# install all needed dependencies.
#Pipfile.lock
# PEP 582; used by e.g. github.com/David-OConnor/pyflow
__pypackages__/
# Celery stuff
celerybeat-schedule
celerybeat.pid
# SageMath parsed files
*.sage.py
# Environments
.env
.venv
env/
venv/
ENV/
env.bak/
venv.bak/
# Spyder project settings
.spyderproject
.spyproject
# Rope project settings
.ropeproject
# mkdocs documentation
/site
# mypy
.mypy_cache/
.dmypy.json
dmypy.json
# Pyre type checker
.pyre/
# pytype static type analyzer
.pytype/
# Cython debug symbols
cython_debug/
### Vim ###
# Swap
[._]*.s[a-v][a-z]
!*.svg # comment out if you don't need vector files
[._]*.sw[a-p]
[._]s[a-rt-v][a-z]
[._]ss[a-gi-z]
[._]sw[a-p]
# Session
Session.vim
Sessionx.vim
# Temporary
.netrwhist
# Auto-generated tag files
tags
# Persistent undo
[._]*.un~
# End of https://www.toptal.com/developers/gitignore/api/ocaml,c,c++,python,vim,emacs,macos
### Nix ###
# nix-build
/result
/result-*
\ No newline at end of file
version=0.19.0
\ No newline at end of file
* 0.3
## 0.4.0 (2021-10-12)
** Features
- New architecture support : ARMv7 Thumb mode
(requires [unisim_archisec](https://github.com/binsec/unisim_archisec))
- New architecture support : AARCH64
(requires [unisim_archisec](https://github.com/binsec/unisim_archisec))
- New architecture support : AMD64
(requires [unisim_archisec](https://github.com/binsec/unisim_archisec))
- Backward Bounded Symbolic Execution (experimental)
- Reworked Static Symbolic Execution
(together with some [documentation](doc/sse/))
** Dropped features (until rework)
- Static Abstract Interpretation
- Dynamic Symbolic Execution
** Misc
- Use Dune build system
- Remove several system dependencies (PIQI, ZMQ)
## 0.3.0 (2020-01-21)
** Features
......@@ -14,9 +38,9 @@
** Misc
- Detach PINSEC to own repository (support to be deprecated in later version)
- Detach PINSEC to own repository (support to be deprecated in later version)
* 0.2 [2018-10-01 Mon]
## 0.2.0 (2018-10-01)
- New symbolic execution engine
- New interpreter for binary code
......@@ -32,6 +56,6 @@
* 0.1 [2017-03-01 Wed]
## 0.1.0 (2017-03-01)
First release
# Contributing to BINSEC
## Public contribution
If you spot a problem with **BINSEC**, documentation or have a feature
request, you can open a new issue using the relevant
[issue form](https://github.com/binsec/binsec/issues).
:information_source:
*Please take note* that we expect the source code and API to change
considerably before we reach version `1.0.0`.
## Joining BINSEC team
Looking for an internship, a PhD, a postdoc or a tenured researcher position,
do not hesitate contact [**BINSEC** seniors](https://binsec.github.io/#people).
##########################################################################
# 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) $(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 $@ $<
# Installing BINSEC from sources
The latest public revision of `binsec` is available on GitHub:
https://github.com/binsec/binsec.
The latest public revision of `unisim_archisec` is available on GitHub:
https://github.com/binsec/unisim_archisec.
A convenient way to build `unisim_archisec` together with `binsec` is to
put `unisim_archisec` directory inside the `binsec` directory.
```console
$ git clone https://github.com/binsec/binsec.git
$ cd binsec
$ git clone https://github.com/binsec/unisim_archisec.git
```
#### Dependencies
##### System
- [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
- [OCaml >= 4.08](https://github.com/ocaml/ocaml)
##### OCaml
- [dune >= 2.8](https://github.com/ocaml/dune)
- [menhir](https://gitlab.inria.fr/fpottier/menhir)
- [ocamlgraph >= 1.8.5](https://github.com/backtracking/ocamlgraph)
- [zarith >= 1.4](https://github.com/ocaml/Zarith)
- *[unisim_archisec](https://github.com/binsec/unisim_archisec) (optional)*
- [odoc](https://github.com/ocaml/odoc) (*documentation*)
- [qcheck](https://github.com/c-cube/qcheck) (*test*)
- [ounit2](https://github.com/gildor478/ounit) (*test*)
## Build instructions
#### With `make`
[Makefile](Makefile) is a wrapper around `dune` build system.
When `opam` is available, using the command `make` will automatically install the missing dependencies.
---
:information_source: **Local opam switch**
If `opam` is available, using the following command will create a new OCaml switch inside the BINSEC tree.
```bash
OCAML_COMPILER=4.08.0 make switch
```
A local switch makes the installation of dependencies, including ocaml supported version, not impacting the system wide ocaml configuration.
*Doing so, everything installed will be readily available but only inside the BINSEC directory.*
---
Run the following in order to build the `binsec` executable:
```bash
make