We provide the instructions to verify our ProVerif code w.r.t. our paper "Remote Attestation with Constrained Disclosure", accepted for publication at the Annual Computer Security Applications Conference (ACSAC) 2023.
In the follwing, we provide the proof-of-concept (PoC) implementation of our RACD Protocol, where we provide instructions to compile and run the code. In addition, we give an overview of our impelementation (see RACD Protocol)
This is the source code used to verify some of the security properties of the Remote Attestation with Constrained Disclosure (RACD) protocol.
The ProVerif
folder contains the ProVerif code (racd.pv
) and the ProVerif Windows executable (proverif.exe
).
racd.pv
: The code is meant to verify the secrecy of the randomness used to blind the template hashes (x_i) from the adversary.
Moreover, we verify if the attacker is able to brute-force/guess x_i.
We verify with ProVerif if the adversary is able to retrieve the values ri and vi through the entire process of the involved entities.
-
Make sure Docker is installed on your system. Under Ubuntu, make sure you are a member of the
docker
group (and either re-login or restart the system after executing the command):sudo usermod -aG docker "${USER}"
-
Clone this Git repository (RACD):
git clone 'https://github.com/DominikRoy/RACD.git'
-
Change to the
ProVerif
foldercd ./ProVerif/
-
Build the Docker image:
./docker/build.sh
-
Either run the RACD ProVerif code non-interactively with:
./docker/run.sh proverif racd.pv
or interactively with:
./docker/run.sh
and then inside the container:
proverif racd.pv
Make sure the following packages are installed:
Install them with:
sudo apt-get install -y ocaml ocaml-compiler-libs ocaml-findlib liblablgtk2-ocaml-dev
-
Download the source of ProVerif for Linux
-
Extract the archive:
tar -xf proverif2.04.tar
-
Navigate to the folder and build the program:
cd proverif2.04 ./build
-
Clone this Git repository into the current folder where the command above was executed.
-
RACD ProVerif code executing the command for Linux:
./proverif RACD/ProVerif/racd.pv
-
Download the ProVerif binary for Windows
-
Clone this Git repository or uncompress the archive.
-
Change to
ProVerif
folder. -
Run our protocol by executing the command for Windows:
proverif.exe racd.pv
We provide instructions to emulate our PoC in Docker with a TPM Simulator. In addition, we describe the commands to deploy our PoC on a real hardware, a Raspberry Pi 3 Model B, and with a real hardware TPM that we used in our experiment evaluation.
The table below gives a small overview of the structure and sub-folders of the racd-protocol
folder. For more details, we refer to racd-protocol readme.
Folder | Content |
---|---|
docker |
The docker folder contains necessary configuration scripts for the Dockerfile in the racd-protocol . For changes or re-use, the Dockerfile needs to be only customized. Hence, the build.sh and run.sh exist to build the image and to run the image. |
example |
The example folder presents cbor files and exemplary certificates. More details can be found in the readme of the racd-protocol . |
include |
The include folder contains all the C - header files. |
src |
The src folder contains the actual implementation of the racd-protocol . For details, we refer to racd-protocol readme. |
-
Make sure Docker is installed on your system. Under Ubuntu, make sure you are a member of the
docker
group (and either re-login or restart the system after executing the command):sudo usermod -aG docker "${USER}"
-
Clone this Git repository (RACD):
git clone 'https://github.com/DominikRoy/RACD.git'
-
Change to the
racd-protocol
foldercd ./racd-protocol/
-
Build the Docker image:
./docker/build.sh
-
Run the RACD container interactively with:
./docker/run.sh
-
Continue with the steps described in Run the RACD Protocol PoC
We need to install an operating system on the Raspberry Pi and configure the TPM. Further, we need to install all dependencies for the RACD Protocol PoC implementation. Finally, we install the RACD Protocol PoC code and set TPM permissions accordingly.
First, we need to prepare the SD card for the Raspberry Pi.
-
Download Raspberry Pi OS:
wget 'https://downloads.raspberrypi.org/raspios_lite_armhf/images/raspios_lite_armhf-2021-11-08/2021-10-30-raspios-bullseye-armhf-lite.zip'
-
Unzip the image:
unzip 2021-10-30-raspios-bullseye-armhf-lite.zip
-
Flash the image:
sudo dd if=2021-10-30-raspios-bullseye-armhf-lite.img of=/dev/sdX status=progress ; sync
-
Mount the SD card.
-
Enable SSH by creating an empty file
ssh
in the boot partition. -
Enable Wifi in the Pi by adding the file
wpa_supplicant.conf
to the boot partition with the following content:country=DE ctrl_interface=DIR=/var/run/wpa_supplicant GROUP=netdev update_config=1 network={ ssid="wifi-name" psk="password" key_mgmt=WPA-PSK }
-
Enable the TPM by editing the
config.txt
of the boot partition (cf. https://letstrust.de/archives/20-Mainline.html):-
Uncomment the line
dtparam=spi=on
. -
Add the line
dtoverlay=tpm-slb9670
at the end of the file.
-
Next, we startup and configure the Raspberry Pi.
-
Insert the SD card into the Raspberry Pi and start it, SSH into it, and run
sudo raspi-config
. Change hostname (racd-pi
), locales, timezone, expand filesystem, etc. -
Copy a SSH public key from you local machine to the Raspberry Pi:
ssh-copy-id -i ~/.ssh/id_rsa.pub pi@racd-pi ## or ssh-copy-id -o PreferredAuthentications=password -o PubkeyAuthentication=no -i ~/.ssh/id_rsa.pub pi@racd-pi ## or forcing, in case only the public key is available ssh-copy-id -o PreferredAuthentications=password -o PubkeyAuthentication=no -f -i some-pub-key.pub pi@racd-pi
-
Disable password login in the
/etc/ssh/sshd_config
file:-
Change the line
#PasswordAuthentication yes
toPasswordAuthentication no
-
Optional: change the line
Port 22
toPort 2784
(or another port) -
Restart SSH with
sudo systemctl restart ssh.service
-
-
Update the package database:
sudo apt update && sudo apt dist-upgrade
-
Install TPM2 TSS dependencies:
sudo apt -y install \ autoconf \ autoconf-archive \ automake \ acl \ build-essential \ doxygen \ gcc \ git \ iproute2 \ libcmocka0 \ libcmocka-dev \ libcurl4-openssl-dev \ libini-config-dev \ libjson-c-dev \ libltdl-dev \ libssl-dev \ libtool \ pkg-config \ procps \ uthash-dev
-
TPM2 TSS: Downlaod, compile, and install:
## clone Git repo git clone --depth=1 -b '3.1.0' \ 'https://github.com/tpm2-software/tpm2-tss.git' ~/tpm2-tss ## compile cd ~/tpm2-tss export LD_LIBRARY_PATH=/usr/local/lib git reset --hard \ && git clean -xdf \ && ./bootstrap \ && ./configure --disable-doxygen-doc \ && make clean \ && make -j ## install sudo make install \ && sudo ldconfig
-
libCoAP: Downlaod, compile, and install:
## clone Git repo git clone --recursive -b 'develop' \ 'https://github.com/obgm/libcoap.git' ~/libcoap cd ~/libcoap git checkout f681525272c1ab2d1abbeed0cfb03edba23d8936 #git checkout ea1deffa6b3997eea02635579a4b7fb7af4915e5 ## compile ./autogen.sh \ && ./configure --disable-tests --disable-documentation --disable-manpages --disable-dtls --disable-shared --enable-fast-install \ && make -j ## install sudo make install \ && sudo ldconfig
-
mbed TLS: Downlaod, compile, and install
## clone Git repo git clone --depth=1 --recursive -b 'v2.25.0' \ 'https://github.com/ARMmbed/mbedtls.git' ~/mbedtls cd ~/mbedtls ## compile make -j lib SHARED=true ## install sudo make install \ && sudo ldconfig
-
QCBOR: Downlaod, compile, and install
## clone Git repo git clone --depth=1 --recursive -b 'v1.1' \ 'https://github.com/laurencelundblade/QCBOR.git' ~/qcbor cd ~/qcbor ## compile make -j all so ## install sudo make install install_so \ && sudo ldconfig
-
t_cose: Downlaod, compile, and install
## clone Git repo git clone --depth=1 --recursive -b 'v1.0.1' \ 'https://github.com/laurencelundblade/t_cose.git' ~/t_cose cd ~/t_cose ## compile make -j -f Makefile.psa libt_cose.a libt_cose.so ## install sudo make -f Makefile.psa install install_so \ && sudo ldconfig
-
Libsodium: Downlaod, compile, and install
## download mkdir libsodium cd libsodium/ wget 'https://github.com/jedisct1/libsodium/releases/download/1.0.18-RELEASE/libsodium-1.0.18.tar.gz' tar xzf libsodium-1.0.18.tar.gz cd libsodium-1.0.18/ ## compile ./configure make -j ## install sudo make install \ && sudo ldconfig
-
Clone this Git repository (RACD):
git clone 'https://github.com/DominikRoy/RACD.git' ~/racd-poc
-
Change to the RACD Protocol PoC folder:
cd ~/racd-poc/racd-protocol/
Set permissions on TPM device:
sudo chmod 777 /dev/tpm*
Continue with the steps described in Run the RACD Protocol PoC
-
Compile:
## clean up make -f Makefileclient clean make -f Makefileserver clean ## build client (verifer) make -f Makefileclient ## build server (attester) make -f Makefileserver
-
Run and collect time information:
## change folder cd example ## export export ASAN_OPTIONS=verify_asan_link_order=0 ## run attester (wait for the output "Waiting for a remote connection ...") ../output/attestor server_name=localhost \ server_port=4433 ca_file=my_ca_localhost.crt \ crt_file=prover_localhost.crt key_file=prover_key.key \ programs_file=programs250.cbor & ## run verifier in a loop for i in {1..100}; do ../output/verifier server_name=localhost \ server_port=4433 ca_file=my_ca_localhost.crt \ crt_file=verifier_localhost.crt key_file=verifier_key.key \ swSelection_file=programs50.cbor; done ## remove log files for next data gathering rm -v pcr0.log ppra_attester_50_local_new.csv ppra_verifier_50_new.csv