Minimal tips to run isolated code

Two frequent motivations for running code in isolation:

1. you want to try it out before installing it,
2. you are writing instructions about installation and need a blank starting point.

The amount of isolation required depends on aspects like trust, host hardware, etc. For most code run by most developers, we can assume the software is not expertly malicious but may have bugs that could break other parts of the local system configuration.

There are several choices for running code in partial or full isolation. Some languages include lightweight environments that do not interfere with each other, e.g., virtual environments in Python. However, due to caching and links, these are not sufficiently isolated for us. At the other end of the spectrum, we can run code in a node of a cloud computing service. However, the overhead and cost make this not worthwhile given our needs: isolation, but not very strong security requirements. Alternatively, we can run a virtual machine or emulator such as QEMU, VirtualBox, or others. This also has too much overhead given our needs.

Thus motivated, install Podman Desktop, a Docker-compatible Linux containers tool with Podman. After Podman Desktop is installed and running, open a terminal and

podman run -it --name demo ubuntu:22.04 bash

which will download an Ubuntu 22.04 base image and start the Bash shell. If you exit the shell, then it can be opened again by

podman start -ai demo

To start another shell inside the same container, open another terminal and

podman exec -it demo bash

Now that you have an isolated environment, let's step through the process of building and running some code inside it. We will do so for Spin, a software verification tool.

First, install Git and a C compiler:

apt update
apt install git build-essential

Then, clone the repository and try to build it:

git clone https://github.com/nimble-code/Spin.git
cd Spin
make

This may end with an error message: make[1]: yacc: No such file or directory. Yacc is a POSIX standard parser generator. Let's install the compatible tool Bison:

apt install bison

Then, try to build Spin again:

make
make install

which will result in spin being added to the system path. Let's run an example:

cd Examples
spin -run sort.pml

The output should show that no errors were found. The file sort.pml models a sorting algorithm in Promela. To confirm that spin is working, we next introduce an error into the model. Copy the example to outside of the container by entering the following in another terminal:

podman cp demo:/Spin/Examples/sort.pml .

Open sort.pml in an editor and, on line 45, change nextval < myval to nextval > myval. Then, copy the file back into the container:

podman cp sort.pml demo:/Spin/Examples/sort.pml

In the terminal with the container, run Spin on the new sort.pml:

spin -run sort.pml

which should show errors: 1, confirming that we introduced a bug.

When you are done with the container, remove it:

podman rm -f demo