From c4f71be8056094293ed4366be447052cb2ca75ed Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 30 Sep 2020 14:36:02 +0200 Subject: [PATCH 1/2] xenci: rename yml to yaml Rename the file for consistency with the other files in this directory. Signed-off-by: Norbert Manthey --- .../workflows/{build-and-test-Xen.yml => build-and-test-Xen.yaml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename .github/workflows/{build-and-test-Xen.yml => build-and-test-Xen.yaml} (100%) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yaml similarity index 100% rename from .github/workflows/build-and-test-Xen.yml rename to .github/workflows/build-and-test-Xen.yaml From 20680de1835798ed9ee4d98fc7632e4d6f66991c Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Wed, 30 Sep 2020 15:01:37 +0200 Subject: [PATCH 2/2] xen-cbmc: fix ci script This script has been broken, and not been picked up in CI until now. This change fixes the script, as well as makes sure that the relevant steps are executed, and the resulting build artefacts have the required goto-cc section in them. This CI script has been refered to as part of the paper: "Using model checking tools to triage the severity of security bugs in the Xen hypervisor", that has been presented at FMCAD 2020. Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 55 +++++++++++++++-------- 1 file changed, 37 insertions(+), 18 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 7aab6780232..6a4cfc408f7 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -1,26 +1,45 @@ -name: Build and Test Xen +name: Build Xen with CPROVER tools -on: [push] +on: + pull_request: + branches: [ develop ] jobs: - Linux: - + CompileXen: runs-on: ubuntu-18.04 - steps: - - name: Install Packages - run: sudo apt-get install coreutils \ - build-essential gcc git make flex bison \ - software-properties-common libwww-perl python \ - bin86 gdb bcc liblzma-dev python-dev gettext iasl \ - uuid-dev libncurses5-dev libncursesw5-dev pkg-config \ - libgtk2.0-dev libyajl-dev sudo time + - uses: actions/checkout@v2 + with: + submodules: true + - name: Install Packages + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get install -y coreutils build-essential gcc git make flex bison software-properties-common libwww-perl python + sudo apt-get install -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config + sudo apt-get install -y libgtk2.0-dev libyajl-dev sudo time + + - name: Build CBMC tools + run: | + make -C src minisat2-download + make -C src cbmc.dir goto-cc.dir goto-diff.dir + + - name: Get one-line-scan + run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git - - uses: actions/checkout@v1 + - name: Get Xen 4.13 + run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 && pwd - - name: build CBMC tools - run: make -C src minisat2-download - run: make -C src cbmc.dir goto-cc.dir goto-diff.dir + - name: Prepare compile Xen with CBMC via one-line-scan + run: | + ln -s goto-cc src/goto-cc/goto-ld + ln -s goto-cc src/goto-cc/goto-as + ln -s goto-cc src/goto-cc/goto-g++ - - name: get Xen 4.13 - run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 + - name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k || true + + - name: Check for goto-cc section in xen-syms binary + run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"