diff --git a/AGENTS.md b/AGENTS.md index 26c101e18698..19997c23609f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -45,7 +45,6 @@ Kani uses [CBMC](https://github.com/diffblue/cbmc) as its underlying verificatio |-----------|-------------| | `docs/` | User and developer documentation (built with mdBook) | | `rfc/` | Request for Comments documents for design decisions | -| `papers/` | Academic papers related to Kani | ## Build and Development Commands diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 000000000000..83f02f8c1c2a --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,75 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +cff-version: 1.2.0 +title: Kani Rust Verifier +message: >- + If you use Kani in your research, please cite the ASE 2026 paper listed under + `preferred-citation`. +type: software +authors: + - name: The Kani Contributors +abstract: >- + Kani is a bit-precise model checker for Rust. It verifies both safety + (undefined behavior) and correctness (panics, arithmetic overflow, and + user-defined properties expressed as assertions or function contracts) of Rust + programs, including unsafe code. +repository-code: https://github.com/model-checking/kani +url: https://model-checking.github.io/kani/ +license: + - Apache-2.0 + - MIT +keywords: + - rust + - model checking + - formal verification + - program analysis + - undefined behavior +preferred-citation: + type: conference-paper + title: "Kani: A Model Checker for Rust" + authors: + - given-names: Rémi + family-names: Delmas + - given-names: Zyad + family-names: Hassan + - given-names: Qinheping + family-names: Hu + - given-names: Rahul + family-names: Kumar + - given-names: Felipe R. + family-names: Monteiro + - given-names: Thanh + family-names: Nguyen + - given-names: Adrián + family-names: Palacios + - given-names: Celina + family-names: Val + - given-names: Michael + family-names: Tautschnig + - given-names: Justus + family-names: Adam + - given-names: Daniel + family-names: Schwartz-Narbonne + - given-names: Carolyn + family-names: Zech + collection-title: >- + Proceedings of the 41st IEEE/ACM International Conference on Automated + Software Engineering (ASE '26) + collection-type: proceedings + conference: + name: >- + 41st IEEE/ACM International Conference on Automated Software Engineering + city: Munich + country: DE + date-start: '2026-10-12' + date-end: '2026-10-16' + publisher: + name: Association for Computing Machinery + city: New York + region: NY + country: US + year: 2026 + month: 10 + pages: 13 + doi: 10.1145/3832783.3834499 + url: https://doi.org/10.1145/3832783.3834499 diff --git a/README.md b/README.md index 4459d5aa25e1..d65d12aae435 100644 --- a/README.md +++ b/README.md @@ -50,6 +50,38 @@ Use Kani in your CI with `model-checking/kani-github-action@VERSION`. See the book](https://model-checking.github.io/kani/install-github-ci.html) for details. +## Citing Kani + +If you use Kani in your research, please cite our ASE 2026 paper. + +ACM Reference Format: + +> Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, and Carolyn Zech. 2026. Kani: A Model Checker for Rust. In *Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE '26), October 12–16, 2026, Munich, Germany*. ACM, New York, NY, USA, 13 pages. + +BibTeX: + +```bibtex +@inproceedings{kani-ase-2026, + author = {Delmas, R{\'e}mi and Hassan, Zyad and Hu, Qinheping and Kumar, Rahul and + Monteiro, Felipe R. and Nguyen, Thanh and Palacios, Adri{\'a}n and + Val, Celina and Tautschnig, Michael and Adam, Justus and + Schwartz-Narbonne, Daniel and Zech, Carolyn}, + title = {{Kani}: A Model Checker for {Rust}}, + year = {2026}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3832783.3834499}, + doi = {10.1145/3832783.3834499}, + booktitle = {Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering}, + numpages = {13}, + location = {Munich, Germany}, + series = {ASE '26} +} +``` + +The same citation is available in machine-readable form in [CITATION.cff](CITATION.cff), +which powers GitHub's *Cite this repository* button. + ## Security See [SECURITY](https://github.com/model-checking/kani/security/policy) for more information. diff --git a/favicon.ico b/favicon.ico deleted file mode 100644 index d2bf13219274..000000000000 Binary files a/favicon.ico and /dev/null differ diff --git a/papers/vstte2024/README.md b/papers/vstte2024/README.md deleted file mode 100644 index 568b501138b5..000000000000 --- a/papers/vstte2024/README.md +++ /dev/null @@ -1 +0,0 @@ -This contains the contents for a short paper at VSTTE2024. In order to build this, please download the LLNCS style file available at https://resource-cms.springernature.com/springer-cms/rest/v1/content/19238648/data/v8, unpack the resulting llncs.zip, and use standard LaTeX tools to build the paper. \ No newline at end of file diff --git a/papers/vstte2024/paper.bib b/papers/vstte2024/paper.bib deleted file mode 100644 index dafdbc98cbb2..000000000000 --- a/papers/vstte2024/paper.bib +++ /dev/null @@ -1,135 +0,0 @@ -% Copyright Kani Contributors -% SPDX-License-Identifier: Apache-2.0 OR MIT - -\begin{paper}{8} -@inproceedings{verus-sys, - author = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan}, - booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)}, - code = {https://github.com/verus-lang/verus}, - month = {November}, - title = {Verus: A Practical Foundation for Systems Verification}, - year = {2024} -} - -@inproceedings{denis2022creusot, - title={Creusot: a foundry for the deductive verification of {R}ust programs}, - author={Denis, Xavier and Jourdan, Jacques-Henri and March{'e}, Claude}, - booktitle={International Conference on Formal Engineering Methods}, - pages={90--105}, - year={2022}, - organization={Springer} -} - -@inproceedings{astrauskas2022prusti, - title={The {P}rusti project: Formal verification for {R}ust}, - author={Astrauskas, Vytautas and B{\'\i}l{\`y}, Aurel and Fiala, Jon{\'a}{\v{s}} and Grannan, Zachary and Matheja, Christoph and M{\"u}ller, Peter and Poli, Federico and Summers, Alexander J}, - booktitle={NASA Formal Methods Symposium}, - pages={88--108}, - year={2022}, - organization={Springer} -} - -@inproceedings{vanhattum2022verifying, - title={Verifying dynamic trait objects in {R}ust}, - author={VanHattum, Alexa and Schwartz-Narbonne, Daniel and Chong, Nathan and Sampson, Adrian}, - booktitle={Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice}, - pages={321--330}, - year={2022} -} - -@manual{superPower, - title = {Unsafe Rust}, - url = {https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html}, - author = {Rust Documentation} -} - -@inproceedings{li2021mirchecker, - title={MirChecker: detecting bugs in {R}ust programs via static analysis}, - author={Li, Zhuohua and Wang, Jincheng and Sun, Mingshen and Lui, John CS}, - booktitle={Proceedings of the 2021 ACM SIGSAC conference on computer and communications security}, - pages={2183--2196}, - year={2021} -} - -@manual{stringChallenge, - title = {Memory Safety of String}, - year = {2024}, - author = {Zyad Hassan}, - url = {https://model-checking.github.io/verify-rust-std/challenges/0010-string.html} -} - -@manual{anderson20medium, - title = {The Rust Compilation Model Calamity}, - year = {2020}, - url = {https://pingcap.medium.com/the-rust-compilation-model-calamity-1a8ce781cf6cb}, - author = {Brian Anderson} -} - -@article{matsakis2014rust, - title={The rust language}, - author={Matsakis, Nicholas D and Klock, Felix S}, - journal={ACM SIGAda Ada Letters}, - volume={34}, - number={3}, - pages={103--104}, - year={2014}, - publisher={ACM New York, NY, USA} -} - -@manual{challenge, - title = {Memory Safety of String}, - url = {https://github.com/model-checking/verify-rust-std/issues/61}, - author = {Zyad Hassan}, - year = {2024} -} - -@manual{solution, - title = {char and ascii{\_}char contracts}, - url = {https://github.com/model-checking/verify-rust-std/pull/48}, - year = {2024}, - author = {Carolyn Zech} -} - -@manual{rustAndroid, - title = {The Impact of Rust on Security Development}, - year = {2024}, - url = {https://www.riscure.com/the-impact-of-rust-on-security-development}, - author = {Christiaan Biesterbosch and Valeria Vatolina} -} -@manual{liam2022android, - title = {How Google is using Rust to reduce memory safety vulnerabilities in Android}, - year = {2020}, - url = {https://www.zdnet.com/article/google-after-using-rust-we-slashed-android-memory-safety-vulnerabilities/}, - author = {Liam Tung} -} - -@article{jung2017rustbelt, - title={RustBelt: Securing the foundations of the Rust programming language}, - author={Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek}, - journal={Proceedings of the ACM on Programming Languages}, - volume={2}, - number={POPL}, - pages={1--34}, - year={2017}, - publisher={ACM New York, NY, USA} -} - -@article{ayoun2024hybrid, - title={A hybrid approach to semi-automated Rust verification}, - author={Ayoun, Sacha-{\'E}lie and Denis, Xavier and Maksimovi{\'c}, Petar and Gardner, Philippa}, - journal={arXiv preprint arXiv:2403.15122}, - year={2024} -} - -@article{ho2022aeneas, - title={Aeneas: Rust verification by functional translation}, - author={Ho, Son and Protzenko, Jonathan}, - journal={Proceedings of the ACM on Programming Languages}, - volume={6}, - number={ICFP}, - pages={711--741}, - year={2022}, - publisher={ACM New York, NY, USA} -} - -\end{thebibliography} \ No newline at end of file diff --git a/papers/vstte2024/paper.tex b/papers/vstte2024/paper.tex deleted file mode 100644 index a523bbf1de5b..000000000000 --- a/papers/vstte2024/paper.tex +++ /dev/null @@ -1,172 +0,0 @@ -% Copyright Kani Contributors -% SPDX-License-Identifier: Apache-2.0 OR MIT - -\documentclass[runningheads]{llncs} -% -\usepackage[T1]{fontenc} -\usepackage{graphicx} -\usepackage{amsmath,amsfonts} -\usepackage{hyperref} -\usepackage{listings} -\usepackage{xcolor} -\usepackage{color} -\usepackage{listings} -\definecolor{GrayCodeBlock}{RGB}{241,241,241} -\definecolor{BlackText}{RGB}{110,107,94} -\definecolor{RedTypename}{RGB}{182,86,17} -\definecolor{GreenString}{RGB}{96,172,57} -\definecolor{PurpleKeyword}{RGB}{184,84,212} -\definecolor{GrayComment}{RGB}{170,170,170} -\definecolor{GoldDocumentation}{RGB}{180,165,45} -\lstdefinelanguage{rust} -{ - columns=fullflexible, - keepspaces=true, - frame=single, - framesep=0pt, - framerule=0pt, - framexleftmargin=4pt, - framexrightmargin=4pt, - framextopmargin=5pt, - framexbottommargin=3pt, - xleftmargin=4pt, - xrightmargin=4pt, - backgroundcolor=\color{GrayCodeBlock}, - basicstyle=\ttfamily\color{BlackText}, - keywords={ - true,false, - unsafe,async,await,move, - use,pub,crate,super,self,mod, - struct,enum,fn,const,static,let,mut,ref,type,impl,dyn,trait,where,as, - break,continue,if,else,while,for,loop,match,return,yield,in - }, - keywordstyle=\color{PurpleKeyword}, - ndkeywords={ - bool,u8,u16,u32,u64,u128,i8,i16,i32,i64,i128,char,str, - Self,Option,Some,None,Result,Ok,Err,String,Box,Vec,Rc,Arc,Cell,RefCell,HashMap,BTreeMap, - macro_rules - }, - ndkeywordstyle=\color{RedTypename}, - comment=[l][\color{GrayComment}\slshape]{//}, - morecomment=[s][\color{GrayComment}\slshape]{/*}{*/}, - morecomment=[l][\color{GoldDocumentation}\slshape]{///}, - morecomment=[s][\color{GoldDocumentation}\slshape]{/*!}{*/}, - morecomment=[l][\color{GoldDocumentation}\slshape]{//!}, - morecomment=[s][\color{RedTypename}]{\#![}{]}, - morecomment=[s][\color{RedTypename}]{\#[}{]}, - stringstyle=\color{GreenString}, - string=[b]" -} - -\begin{document} -% -\title{Verifying the Rust Standard Library} -%\titlerunning{Verifying the Rust} - -\author{ -Rahul Kumar \and -Celina Val \and -Felipe Monteiro \and -Michael Tautschnig \and -Zyad Hassan \and -Qinheping Hu \and -Adrian Palacios \and -Remi Delmas \and -Jaisurya Nanduri \and -Felix Klock \and -Justus Adam \and -Carolyn Zech \and -Artem Agvanian -} -% -\authorrunning{R. Kumar et al.} - -\institute{Amazon Web Services, USA\\ \url{https://aws.amazon.com/} -} - -\maketitle - -\begin{abstract} -The Rust programming language is growing fast and seeing increased adoption due to performance and speed-of-development benefits. It provides strong compile-time guarantees along with blazing performance and an active community of support. The Rust language has experienced steady growth in the last few years with a total developer size of close to 3M developers. Several large projects such as Servo, TiKV, and the Rust compiler itself are in the millions of lines of code. Although Rust provides strong safety guarantees for \texttt{safe} code, the story with \texttt{unsafe} code is incomplete. In this short paper, we motivate the case for verifying the Rust standard library and how we are approaching this endeavor. We describe our effort to verify the Rust standard library via a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges open to all. - -\keywords{Rust \and standard library \and verification \and formal methods \and safe -\and unsafe \and memory safety \and correctness \and challenge} -\end{abstract} - -\section{Rust} - -Rust~\cite{matsakis2014rust} is a modern programming language designed to enable developers to efficiently create high performance reliable systems. Rust delivers high performance because it does not use a garbage collector. Combined with a powerful type system that enforces ownership of memory wherein memory can be shared or mutable, but never both. This helps avoid data-races and memory errors, thereby reducing the trade-off between high-level safety guarantees and low-level controls -- a highly desired property of programming languages. Unlike C/C++, the Rust language aims to minimize undefined behavior statically by employing a strong type system and an \textit{extensible} ownership model for memory. - -The extensible model of ownership relies on the simple (yet difficult) principle of enforcing that an object can be accessed by multiple aliases/references only for read purposes. To write to an object, there can only be one reference to it at any given time. Such a principle in practice eliminates significant amounts of memory-related errors~\cite{rustAndroid}. In spite of the great benefits in practice, this principle tends to be restrictive for a certain subset of implementations that are too low-level or require very specific types of synchronization. As a result, the Rust language introduced the \texttt{unsafe} keyword. When used, the compiler may not be able to prove the memory safety rules that are enforced on \texttt{safe} code blocks. Alias tracking is not performed for raw pointers which can only be used in \texttt{unsafe} code blocks, which enables developers to perform actions that would be rejected by the compiler in \texttt{safe} code blocks. This is also referred to as \textit{superpowers}~\cite{superPower} of \texttt{unsafe} code blocks. Examples of these superpowers include dereferencing a raw pointer, calling an unsafe function or method, and accessing fields of unions etc. A clear side-effect of this choice is that most if not all memory related errors in the code are due to the \texttt{unsafe} code blocks introduced by the developer. - -Rust developers use \textit{encapsulation} as a common design pattern to mask unsafe code blocks. The safe abstractions allow \texttt{unsafe} code blocks to be limited in number and not leak into all parts of the codebase. The Rust standard library itself has widespread use of \texttt{unsafe} code blocks, with almost 5.5K \texttt{unsafe} functions and 4.8K \texttt{unsafe} code blocks. In the last 3 years, 40 soundness issues have been filed in the Rust standard library along with 17 reported CVEs, even with the extensive testing and usage of the library. The onus of proving the safety and correctness of these \texttt{unsafe} code blocks is on the developers. Some such efforts have been made, but there is still a lot of ground to cover~\cite{jung2017rustbelt}. - -Verifying the Rust standard library is important and rewarding along multiple dimensions such as improving Rust, creating better verification tools, and enabling a safer ecosystem. Given the size and scope of this exercise, we believe doing this in isolation would be expensive and counter-productive. Ergo, we believe that motivating the community and creating a unified crowd-sourced effort is the desirable method, which we hope to catalyze via our proposed effort. - - -\section{Rust Verification Landscape} - -A common misconception Rust developers have is that they are producing \texttt{safe} memory-safe code by simply using Rust as their development language. To counter this, there have been significant efforts to create tools and techniques that enable verification of Rust code. Here we list (alphabetically) some tools: - -\begin{itemize} - - \item \textbf{Creusot}~\cite{denis2022creusot} is a Rust verifier that also employs deductive-style verification for \texttt{safe} Rust code. Creusot also introduces \textbf{Pearlite} - a specification language for specifying function and loop contracts. - - \item \textbf{Gillian-Rust}~\cite{ayoun2024hybrid} is a separation logic based hybrid verification tool for Rust programs with support for \texttt{unsafe} code. Gillian-Rust is also linked to Creusot, but does in certain cases require manual intervention. - - \item \textbf{Kani}~\cite{vanhattum2022verifying} uses bounded model checking to verify generic memory safety properties and user specified assertions. Kani supports both \texttt{unsafe} and \texttt{safe} code, but cannot guarantee unbounded verification in all cases. - - \item \textbf{Prusti}~\cite{astrauskas2022prusti} employs deductive verification to prove functional correctness of \texttt{safe} Rust code. Specifically, it targets certain type of \textit{panics} and allows users to specify properties of interest. - - \item \textbf{Verus}~\cite{verus-sys} is an SMT-based tool used to verify Rust code and can support \texttt{unsafe} in certain situations such as the use of raw pointers and unsafe cells. - - \item There are several other tools which are in the related space, but we do not list them here explicitly. -\end{itemize} - -\section{Verifying the Rust Standard Library} - -We are proposing the creation of a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges. Each challenge describes the goal and the success criteria. Currently, we are focusing on doing verification for memory-safety. The challenges are open to anyone. This effort aims to be \textit{tool agnostic} to facilitate the introduction of verification solutions into the Rust mainline and making verification an integral part of the Rust ecosystem. Towards this, we have been working with the Rust language team to introduce function and loop contracts into the Rust mainline and have created a fork of the Rust standard library repository \url{https://github.com/model-checking/verify-rust-std/} wherein all solutions to challenges and verification artifacts are stored. Challenges can come in various flavors: 1/ specifying contracts for a part of the Rust standard library, 2/ specify and verify a part of the Rust standard library, and 3/ introduce new tools/techniques to verify parts of the Rust standard library. The repository provides templates for introducing new challenges, new tools, and instructions on how to submit solutions to challenges. To date, we have over 20 students, academics, and researchers engaging. - -As part of this effort, we are also creating challenges. For example, we have created a challenge to verify the String library in the standard library~\cite{stringChallenge}. In this challenge, the goal is to verify the memory safety of \texttt{std::string::String} and prove the absence of undefined behavior (UB). Even though the majority of \texttt{String} methods are safe, many of them are safe abstractions over unsafe code. For instance, the insert method is implemented as follows : -\begin{lstlisting}[language=rust, caption=Unsafe usage in String, frame=single, numbers=left] - pub fn insert(&mut self, idx: usize, ch: char) { - assert!(self.is_char_boundary(idx)); - let mut bits = [0; 4]; - let bits = ch.encode_utf8(&mut bits).as_bytes(); - - unsafe { - self.insert_bytes(idx, bits); - } - } -\end{lstlisting} - -The goal also specifies the \textit{success criteria} that must be met for the solution to be reviewed and merged into the CI pipeline. -\begin{lstlisting}[caption=Success criteria for the String challenge.,frame=single] -Verify the memory safety of all public functions that are -safe abstractions over unsafe code: - unbounded: from_utf16le, from_utf16le_lossy, - from_utf16be, from_utf16be_lossy, - remove_matches, insert_str, - split_off, replace_range, retain - others: pop, remove, insert, drain, leak, - into_boxed_str -Ones marked as unbounded must be verified for any -string/slice length. -\end{lstlisting} - -Example of a solution for a challenge can be found in~\cite{solution}. This particular solution introduces new contracts for \texttt{char} and \texttt{ascii\_char}. The contracts are also verified using Kani. - -\noindent \textbf{Our call to action} to you is to come and be a part of this effort and contribute by solving challenges, introducing new challenges, introducing new tools, or helping review and refine the current processes! - -\begin{credits} -\subsubsection{\ackname} We would like to thank all the academic partners that have helped us shape challenges, started contributing to challenges, and provide invaluable advice throughout the process of jump starting this initiative. We also would like to thank Niko Matsakis, Byron Cook, and Kurt Kufeld for their support and leadership. -\end{credits} - -% -% Bibliography -% -\bibliographystyle{splncs04} -\bibliography{paper} - - -\end{document} diff --git a/scripts/ci/Dockerfile.bundle-test-al2 b/scripts/ci/Dockerfile.bundle-test-al2 deleted file mode 100644 index 4e18f2165e90..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-al2 +++ /dev/null @@ -1,19 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM amazonlinux:2 -RUN yum install -y gcc curl tar gzip && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -#RUN cargo install --path ./kani-verifier -#RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz -RUN cargo install kani-verifier -RUN cargo-kani setup diff --git a/scripts/ci/Dockerfile.bundle-test-nixos b/scripts/ci/Dockerfile.bundle-test-nixos deleted file mode 100644 index 2bbeb8ceee18..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-nixos +++ /dev/null @@ -1,41 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM nixos/nix -RUN nix-channel --update -WORKDIR /tmp/kani -RUN echo $' \n\ -with import {}; \n\ -mkShell { \n\ - packages = [ \n\ - curl \n\ - gcc \n\ - patchelf \n\ - rustup \n\ - ]; \n\ -}' >> ./default.nix -# we need to switch to nix-shell to get proper support for e.g. pip -SHELL ["nix-shell", "--command"] -ENTRYPOINT ["nix-shell"] -RUN rustup toolchain add stable -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz - -# Temporary hack: nix-shell causes problems when trying to run these with 'docker run' -# like we do for other tests, so we've imported these into the dockerfile for now -# until everything can be replaced with 'self-test': -# https://github.com/model-checking/kani/issues/1246 -RUN cargo kani --version -RUN (cd /tmp/kani/tests/cargo-kani/simple-lib && cargo kani) -RUN (cd /tmp/kani/tests/cargo-kani/simple-visualize && cargo kani) -RUN (cd /tmp/kani/tests/cargo-kani/build-rs-works && cargo kani) -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 deleted file mode 100644 index f81af91f6f52..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:20.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-*.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt deleted file mode 100644 index 35bc522b651f..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt +++ /dev/null @@ -1,22 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle -# using an alternative install path * - -FROM ubuntu:20.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true \ - KANI_HOME="/tmp" -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-*.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 deleted file mode 100644 index f7dd23e1233d..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:22.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 deleted file mode 100644 index 1b85fd2e0b58..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:24.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/README.md b/scripts/ci/README.md new file mode 100644 index 000000000000..0bbc92c36fd4 --- /dev/null +++ b/scripts/ci/README.md @@ -0,0 +1,45 @@ +# CI helpers + +Helper scripts and container definitions used by the GitHub Actions workflows in +[`.github/workflows/`](../../.github/workflows). Nothing here is part of a normal +local build. + +## `Dockerfile.bundle-release-24-04` + +Builds the container image published for each Kani release, +`ghcr.io/model-checking/kani-ubuntu-24.04:` (also tagged `latest`). + +It is used by the `Package Docker` job in +[`release.yml`](../../.github/workflows/release.yml), which runs only on pushes of a +`kani-*` tag. That job produces the release artifacts first, then builds this image +with the repository root as the build context — so the root +[`.dockerignore`](../../.dockerignore) is what keeps `.git`, `firecracker/`, and +`target/{debug,release}` out of the uploaded context — and pushes the result to GHCR. + +Because it installs Kani *from those artifacts* rather than from source, it cannot be +built from a clean checkout. Two things must already exist in the build context: + +| Path in the build context | Produced by | +|---------------------------|-------------| +| `kani--x86_64-unknown-linux-gnu.tar.gz` | `cargo bundle` | +| `target/package/kani-verifier-/` | `cargo package -p kani-verifier` | + +To reproduce the release image locally: + +```bash +cargo bundle +cargo package -p kani-verifier +docker build -t kani-ubuntu-24.04 -f scripts/ci/Dockerfile.bundle-release-24-04 . +``` + +Note that installing a release bundle is *not* tested through Docker. The `TestBundle` +job in `release.yml` does that natively across the macOS and Ubuntu runners it supports. + +## Copyright check + +`run-copyright-check.sh` runs `copyright_check.py` over every tracked file that does not +match a pattern in `copyright-exclude`, requiring the two-line header described in +[`docs/src/conventions.md`](../../docs/src/conventions.md). It runs in the +`format-check` workflow. + +The script uses `xargs -d`, which is GNU-only, so it does not run as-is on macOS.