Skip to content

Commit d6f12dd

Browse files
cgwalterscgwalters
committed
devenv: Add Kani and extract shared installation scripts
Add Kani formal verification tool - a bounded model checker for Rust that can verify safety properties and absence of undefined behavior. Kani requires rustup because it bundles a specific nightly toolchain. Also deduplicate the installation logic between c10s and debian Containerfiles by extracting into shared shell scripts: - fetch-tools.sh: Downloads bcvk and scorecard binaries - install-rust.sh: Installs rustup/cargo system-wide to /usr/local - install-kani.sh: Installs kani formal verification tool Key changes: - Add rustup symlink at $CARGO_HOME/bin/rustup (required for rustup's self-update check which looks for itself there) - Add new 'kani' build stage that compiles kani-verifier and runs setup - Set KANI_HOME=/usr/local/kani for system-wide installation - Copy kani bundle (compiler, libraries, CBMC) to final image The kani version is renovate-managed via the kaniversion ARG. Assisted-by: OpenCode (Claude Sonnet 4) Signed-off-by: Colin Walters <walters@verbum.org>
1 parent dda396b commit d6f12dd

6 files changed

Lines changed: 125 additions & 106 deletions

File tree

‎devenv/.dockerignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,6 @@
1212
!build-deps-debian.txt
1313
!build-deps-c10s.txt
1414
!devenv-init.sh
15+
!fetch-tools.sh
16+
!install-rust.sh
17+
!install-kani.sh

‎devenv/Containerfile.c10s‎

Lines changed: 18 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -30,59 +30,20 @@ FROM base as tools
3030
ARG bcvkversion=v0.9.0
3131
# renovate: datasource=github-releases depName=ossf/scorecard
3232
ARG scorecardversion=v5.1.1
33-
RUN <<EORUN
34-
set -xeuo pipefail
35-
arch=$(arch)
36-
37-
rm -vrf /usr/local/bin/*
38-
39-
# bcvk
40-
if test "${arch}" = x86_64; then
41-
td=$(mktemp -d)
42-
(
43-
cd $td
44-
target=bcvk-${arch}-unknown-linux-gnu
45-
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
46-
tar xvzf $target.tar.gz
47-
mv $target /usr/local/bin/bcvk
48-
)
49-
rm -rf $td
50-
else
51-
echo bcvk unavailable for $arch
52-
fi
53-
54-
# scorecard (OpenSSF security scanner)
55-
td=$(mktemp -d)
56-
(
57-
cd $td
58-
# Map arch to scorecard naming convention
59-
case "${arch}" in
60-
x86_64) scarch=amd64 ;;
61-
aarch64) scarch=arm64 ;;
62-
*) echo "scorecard unavailable for $arch"; exit 0 ;;
63-
esac
64-
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
65-
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
66-
tar xvzf $target
67-
mv scorecard /usr/local/bin/scorecard
68-
)
69-
rm -rf $td
70-
EORUN
33+
COPY fetch-tools.sh /run/src/
34+
RUN bcvkversion=$bcvkversion scorecardversion=$scorecardversion /run/src/fetch-tools.sh
7135

7236
FROM base as rust
73-
RUN <<EORUN
74-
set -xeuo pipefail
75-
# Setup rust; the idea here though is we install system-wide into /usr/local
76-
# as if it was packaged.
77-
export RUSTUP_HOME=/usr/local/rustup
78-
export CARGO_HOME=/usr/local/cargo
79-
# Install Rust system-wide
80-
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
81-
# Move binaries to /usr/local/bin (system-managed, root-owned)
82-
mv /usr/local/cargo/bin/* /usr/local/bin/
83-
# Nothing really left here
84-
rm -vrf /usr/local/cargo/bin
85-
EORUN
37+
COPY install-rust.sh /run/src/
38+
RUN /run/src/install-rust.sh
39+
40+
# Kani formal verification tool - requires rustup for toolchain management
41+
FROM rust as kani
42+
# renovate: datasource=crate depName=kani-verifier
43+
ARG kaniversion=0.67.0
44+
RUN dnf install -y gcc && dnf clean all
45+
COPY install-kani.sh /run/src/
46+
RUN kaniversion=$kaniversion /run/src/install-kani.sh
8647

8748
# This builds the image.
8849
# Build this using `just devenv-build-c10s` from the root of the repository.
@@ -100,10 +61,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
10061

10162
# Copy in the binaries from our tools container image
10263
COPY --from=tools /usr/local/bin/* /usr/local/bin/
103-
COPY --from=rust /usr/local/bin/* /usr/local/bin/
104-
COPY --from=rust /usr/local/rustup /usr/local/rustup
64+
COPY --from=kani /usr/local/bin/* /usr/local/bin/
65+
COPY --from=kani /usr/local/rustup /usr/local/rustup
66+
# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
67+
COPY --from=kani /usr/local/kani /usr/local/kani
10568
# Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
10669
ENV RUSTUP_HOME=/usr/local/rustup
70+
# Point Kani at the system-wide installation
71+
ENV KANI_HOME=/usr/local/kani
10772
# Setup for codespaces
10873
COPY devenv-init.sh /usr/local/bin/
10974

‎devenv/Containerfile.debian‎

Lines changed: 18 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -30,59 +30,20 @@ FROM base as tools
3030
ARG bcvkversion=v0.9.0
3131
# renovate: datasource=github-releases depName=ossf/scorecard
3232
ARG scorecardversion=v5.1.1
33-
RUN <<EORUN
34-
set -xeuo pipefail
35-
arch=$(arch)
36-
37-
rm -vrf /usr/local/bin/*
38-
39-
# bcvk
40-
if test "${arch}" = x86_64; then
41-
td=$(mktemp -d)
42-
(
43-
cd $td
44-
target=bcvk-${arch}-unknown-linux-gnu
45-
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
46-
tar xvzf $target.tar.gz
47-
mv $target /usr/local/bin/bcvk
48-
)
49-
rm -rf $td
50-
else
51-
echo bcvk unavailable for $arch
52-
fi
53-
54-
# scorecard (OpenSSF security scanner)
55-
td=$(mktemp -d)
56-
(
57-
cd $td
58-
# Map arch to scorecard naming convention
59-
case "${arch}" in
60-
x86_64) scarch=amd64 ;;
61-
aarch64) scarch=arm64 ;;
62-
*) echo "scorecard unavailable for $arch"; exit 0 ;;
63-
esac
64-
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
65-
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
66-
tar xvzf $target
67-
mv scorecard /usr/local/bin/scorecard
68-
)
69-
rm -rf $td
70-
EORUN
33+
COPY fetch-tools.sh /run/src/
34+
RUN bcvkversion=$bcvkversion scorecardversion=$scorecardversion /run/src/fetch-tools.sh
7135

7236
FROM base as rust
73-
RUN <<EORUN
74-
set -xeuo pipefail
75-
# Setup rust; the idea here though is we install system-wide into /usr/local
76-
# as if it was packaged.
77-
export RUSTUP_HOME=/usr/local/rustup
78-
export CARGO_HOME=/usr/local/cargo
79-
# Install Rust system-wide
80-
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
81-
# Move binaries to /usr/local/bin (system-managed, root-owned)
82-
mv /usr/local/cargo/bin/* /usr/local/bin/
83-
# Nothing really left here
84-
rm -vrf /usr/local/cargo/bin
85-
EORUN
37+
COPY install-rust.sh /run/src/
38+
RUN /run/src/install-rust.sh
39+
40+
# Kani formal verification tool - requires rustup for toolchain management
41+
FROM rust as kani
42+
# renovate: datasource=crate depName=kani-verifier
43+
ARG kaniversion=0.67.0
44+
RUN apt-get update && apt-get install -y --no-install-recommends gcc libc6-dev && rm -rf /var/lib/apt/lists/*
45+
COPY install-kani.sh /run/src/
46+
RUN kaniversion=$kaniversion /run/src/install-kani.sh
8647

8748
# This builds the image.
8849
# Build this using `just devenv-build-debian` from the root of the repository.
@@ -100,10 +61,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
10061

10162
# Copy in the binaries from our tools container image
10263
COPY --from=tools /usr/local/bin/* /usr/local/bin/
103-
COPY --from=rust /usr/local/bin/* /usr/local/bin/
104-
COPY --from=rust /usr/local/rustup /usr/local/rustup
64+
COPY --from=kani /usr/local/bin/* /usr/local/bin/
65+
COPY --from=kani /usr/local/rustup /usr/local/rustup
66+
# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
67+
COPY --from=kani /usr/local/kani /usr/local/kani
10568
# Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
10669
ENV RUSTUP_HOME=/usr/local/rustup
70+
# Point Kani at the system-wide installation
71+
ENV KANI_HOME=/usr/local/kani
10772
# Setup for codespaces
10873
COPY devenv-init.sh /usr/local/bin/
10974

‎devenv/fetch-tools.sh‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#!/bin/bash
2+
# Fetch architecture-independent binary tools into /usr/local/bin
3+
# This script is shared between c10s and debian container builds.
4+
set -xeuo pipefail
5+
6+
# Required environment variables (passed as build ARGs)
7+
: "${bcvkversion:?bcvkversion is required}"
8+
: "${scorecardversion:?scorecardversion is required}"
9+
10+
arch=$(arch)
11+
12+
rm -vrf /usr/local/bin/*
13+
14+
# bcvk
15+
if test "${arch}" = x86_64; then
16+
td=$(mktemp -d)
17+
(
18+
cd $td
19+
target=bcvk-${arch}-unknown-linux-gnu
20+
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
21+
tar xvzf $target.tar.gz
22+
mv $target /usr/local/bin/bcvk
23+
)
24+
rm -rf $td
25+
else
26+
echo bcvk unavailable for $arch
27+
fi
28+
29+
# scorecard (OpenSSF security scanner)
30+
td=$(mktemp -d)
31+
(
32+
cd $td
33+
# Map arch to scorecard naming convention
34+
case "${arch}" in
35+
x86_64) scarch=amd64 ;;
36+
aarch64) scarch=arm64 ;;
37+
*) echo "scorecard unavailable for $arch"; exit 0 ;;
38+
esac
39+
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
40+
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
41+
tar xvzf $target
42+
mv scorecard /usr/local/bin/scorecard
43+
)
44+
rm -rf $td

‎devenv/install-kani.sh‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#!/bin/bash
2+
# Install Kani formal verification tool
3+
# This script is shared between c10s and debian container builds.
4+
# Prerequisites: rustup must already be installed (via install-rust.sh)
5+
set -xeuo pipefail
6+
7+
# Required environment variable (passed as build ARG)
8+
: "${kaniversion:?kaniversion is required}"
9+
10+
export RUSTUP_HOME=/usr/local/rustup
11+
export CARGO_HOME=/usr/local/cargo
12+
export PATH="/usr/local/bin:$PATH"
13+
14+
# Install Kani to a system-wide location so all users can access it
15+
export KANI_HOME=/usr/local/kani
16+
17+
# Install kani-verifier
18+
/bin/time -f '%E %C' cargo install --locked kani-verifier --version $kaniversion
19+
20+
# Run kani setup - downloads bundle and installs required nightly toolchain
21+
/bin/time -f '%E %C' /usr/local/cargo/bin/cargo-kani setup
22+
23+
# Move kani binaries to /usr/local/bin, keep rustup symlink
24+
mv /usr/local/cargo/bin/cargo-kani /usr/local/cargo/bin/kani /usr/local/bin/

‎devenv/install-rust.sh‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#!/bin/bash
2+
# Install Rust system-wide into /usr/local
3+
# This script is shared between c10s and debian container builds.
4+
set -xeuo pipefail
5+
6+
export RUSTUP_HOME=/usr/local/rustup
7+
export CARGO_HOME=/usr/local/cargo
8+
9+
# Install Rust system-wide
10+
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
11+
12+
# Move binaries to /usr/local/bin (system-managed, root-owned)
13+
mv /usr/local/cargo/bin/* /usr/local/bin/
14+
15+
# Recreate bin directory with symlink to rustup - rustup's self-update check
16+
# looks for itself at $CARGO_HOME/bin/rustup
17+
mkdir -p /usr/local/cargo/bin
18+
ln -sf /usr/local/bin/rustup /usr/local/cargo/bin/rustup

0 commit comments

Comments
 (0)