diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index c52a4b9..2c386d8 100644 --- a/.github/workflows/book.yml +++ b/.github/workflows/book.yml @@ -1,10 +1,41 @@ -name: Deploy mdBook +env: + cache_generation: 2024-03-04 + +name: Deploy site + on: [push] + jobs: build: runs-on: ubuntu-latest + env: + ZOLA_VERSION: 0.16.0 steps: - - uses: actions/checkout@v2 - - uses: XAMPPRocky/deploy-mdbook@v1.1 - with: - token: ${{ secrets.GITHUB_TOKEN }} + - uses: actions/checkout@v3 + - name: Install Zola + run: | + curl -sL https://github.com/getzola/zola/releases/download/v${ZOLA_VERSION}/zola-v${ZOLA_VERSION}-x86_64-unknown-linux-gnu.tar.gz | tar xz -C /usr/local/bin + - name: Build with Zola + run: | + zola build --drafts + zola build + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 + with: + path: ./public + deploy: + needs: build + + permissions: + pages: write + id-token: write + + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + + runs-on: ubuntu-latest + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 # or specific "vX.X.X" version tag for this action \ No newline at end of file diff --git a/book.toml b/book.toml deleted file mode 100644 index 7c2181b..0000000 --- a/book.toml +++ /dev/null @@ -1,14 +0,0 @@ -[book] -authors = ["Rust Formal Methods Interest Group"] -language = "en" -multilingual = false -src = "src" -title = "Rust Formal Methods Interest Group" - -[output.html] -site-url = "/" -git-repository-url = "https://github.com/rust-formal-methods/rust-formal-methods.github.io" - -[output.html.fold] -enable = true -level = 0 diff --git a/config.toml b/config.toml new file mode 100644 index 0000000..9474649 --- /dev/null +++ b/config.toml @@ -0,0 +1,20 @@ +# The URL the site will be built for +base_url = "https://rust-formal-methods.github.io" + +# Whether to automatically compile all Sass files in the sass directory +compile_sass = true + +# Whether to build a search index to be used later on by a JavaScript library +build_search_index = false + +theme = "anemone" + +title = "Rust Formal Methods Interest Group" + +[markdown] +# Whether to do syntax highlighting +# Theme can be customised by setting the `highlight_theme` variable to a theme supported by Zola +highlight_code = true + +[extra] +# Put all your custom variables here diff --git a/content/meetings/_index.md b/content/meetings/_index.md new file mode 100644 index 0000000..49bea83 --- /dev/null +++ b/content/meetings/_index.md @@ -0,0 +1,4 @@ ++++ +title = "RFMIG meetings" ++++ +meetings section \ No newline at end of file diff --git a/content/meetings/contracts.md b/content/meetings/contracts.md new file mode 100644 index 0000000..69e8844 --- /dev/null +++ b/content/meetings/contracts.md @@ -0,0 +1,29 @@ ++++ +title = "Contracts in Rust" +date = 2024-09-24 ++++ +**Title**: + +**Abstract**: + +As the growing number of verification tools (Aeneas, Creusot, Kani, Prusti, Verus, ...) has shown, there is a growing community for formal verification of Rust code. +Each of these tools needs to re-invent a specification language, leading to a rapidly fragmenting ecosystem of incompatible languages and tools. +To address this and related challenges, a Major Change Proposal was proposed to integrate support for contracts and invariants into Rust. +But what does this mean? + +Today, current tools must either embed a whole additional specification language via macros, or attemt to parse contracts from `assert!` and related features. +Both solutions leave a lot to be desired, as this makes it difficult for users to use these tools, while also hindering the development of said tools. +It also means that each tool has its own language, making interoperability hard. + +The shiny future we are aiming for is one in which ordinary Rust programmers are writing contracts as part of every day Rust to be verified with dynamic (and static) tools. +Rather than building their codebase around a single verifier, they can just "plug in" different verifiers, reusing the majority of their contracts. + +In this talk we present a vision for how we might get to this future, and some of the steps we can take on the way there. + +**Presenter**: + +Felix has been working on the Rust compiler since before Rust 1.0; he was co-lead of the Rust compiler team from 2019 until 2023. Felix has taken on this work as part of a broader interest in enforcing safety and correctness properties for Rust code. + +**Meeting Link**: + +**Recording Link**: \ No newline at end of file diff --git a/src/SUMMARY.md b/src/SUMMARY.md deleted file mode 100644 index 9927280..0000000 --- a/src/SUMMARY.md +++ /dev/null @@ -1,4 +0,0 @@ -- [Welcome](./welcome.md) -- [Tools](./tools.md) -- [Previous Events](./previous-events.md) -- [Code of Conduct](./coc.md) diff --git a/src/coc.md b/src/coc.md deleted file mode 100644 index 7ac27ff..0000000 --- a/src/coc.md +++ /dev/null @@ -1,21 +0,0 @@ -# 💖 Code of conduct - -## Rust code of conduct -All participants in the Rust Formal Methods IG meeting are expected to observe the [Rust code of conduct](https://www.rust-lang.org/policies/code-of-conduct). - -* We are committed to providing a friendly, safe and welcoming environment for all, regardless of level of experience, gender identity and expression, sexual orientation, disability, personal appearance, body size, race, ethnicity, age, religion, nationality, or other similar characteristic. -* Please avoid using overtly sexual aliases or other nicknames that might detract from a friendly, safe and welcoming environment for all. -* Please be kind and courteous. There’s no need to be mean or rude. -* Respect that people have differences of opinion and that every design or implementation choice carries a trade-off and numerous costs. There is seldom a right answer. -* Please keep unstructured critique to a minimum. If you have solid ideas you want to experiment with, make a fork and see how it works. -* We will exclude you from interaction if you insult, demean or harass anyone. That is not welcome behavior. We interpret the term “harassment” as including the definition in the [Citizen Code of Conduct](https://github.com/stumpsyn/policies/blob/master/citizen_code_of_conduct.md); if you have any lack of clarity about what might be included in that concept, please read their definition. In particular, we don’t tolerate behavior that excludes people in socially marginalized groups. -* Private harassment is also unacceptable. No matter who you are, if you feel you have been or are being harassed or made uncomfortable by a community member, please contact `xldenis@lri.fr` immediately. Whether you’re a regular contributor or a newcomer, we care about making this community a safe place for you and we’ve got your back. -* Likewise any spamming, trolling, flaming, baiting or other attention-stealing behavior is not welcome. - -## Rust Formal Methods IG Rules for participation - -Please observe the [meeting rules for participation](./meetings.md#rules-for-participation). - -## Moderation contact - -Please contact `xldenis@lri.fr`. \ No newline at end of file diff --git a/src/previous-events.md b/src/previous-events.md deleted file mode 100644 index 6b2ba72..0000000 --- a/src/previous-events.md +++ /dev/null @@ -1,116 +0,0 @@ -## Previous Meetings - - - -### October Meeting (October 24th, 2022) - -#### Abstract - -We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on *functional* properties of their code. - -[Video]( https://youtu.be/9j9EE36lJJI ) - -### September Meeting (September 26th, 2022) - -#### Abstract -This talk describes CreuSAT, a formally verified SAT solver written in Rust. In addition to implementing the core conflict-driven clause learning (CDCL) algorithm, CreuSAT also implements a series of crucial optimizations. -The most important of these is the two watched literals scheme with blocking literals and circular search, the variable move-to-front (VMTF) decision heuristic, clause deletion, phase saving, and moving average based restarts. - -The resulting solver is the first deductively verified solver which is able to consistently solve problems from the SAT competition. -This is done while maintaining a relatively small code base, amounting to around 4 thousand lines of proof code and program code combined, with a low proof overhead of around three lines of proof code per line of program code. - -[Video]( https://youtu.be/MkhjDpai8fM ) - -### June Meeting (June 27th, 2022) - -#### Abstract -Statically analyzing information flow, or how data influences other data within a program, is a challenging task in languages with mutation and pointers. Prior work addressed these challenges with bespoke type systems to encode information flow, such as in JFlow (for Java) and FlowCaml (for OCaml). We demonstrate that Rust's existing system of ownership types can repurposed for modular information flow analysis. We describe our analysis using Oxide, a formal model of safe Rust, and prove its soundness as noninterference. We implement the analysis as Flowistry, a tool that analyzes information flow within Rust's MIR CFG. And we show that Flowistry is reasonably precise versus a whole-program analysis via an evaluation on a dataset of large Rust codebases. - -#### About the Speaker -Will Crichton is a 6th year CS Ph.D. student at Stanford University advised by Profs. Pat Hanrahan and Maneesh Agrawala. His research combines programming language theory and cognitive psychology to build better tools for programmers. Will just defended his thesis, "Revisiting Program Slicing with Ownership-based Information Flow", and will soon be starting a postdoc with Shriram Krishnamurthi at Brown to study the learnability of Rust. - -[Video](https://youtu.be/adDGcSSZKI4) - -### May Meeting (May 30th, 2022) - -#### Abstract -crux-mir is a symbolic testing tool for Rust. The user writes test cases using symbolic variables as inputs; crux-mir uses symbolic execution to check that the tests pass for all possible values of the symbolic variables. crux-mir checks for absence of panics, overflows, and some forms of undefined behavior, and it supports user-defined assertions. Recently, crux-mir gained support for calling Cryptol specifications directly from Rust code and for compositional reasoning, which allows efficiently verifying more complex functions, such as Rust implementations of cryptographic primitives. -In this talk, I'll describe the design of crux-mir and show some examples of its use, with particular focus on the newer Cryptol and compositional reasoning features. - -[Video](https://www.youtube.com/watch?v=f3b5V3B4Q8c) - -### April Meeting (April 25th, 2022) - -#### Abstract - -Ferrocene is an effort to bring Rust into the realm of safety-critical software while also bringing tangible benefits to so called mission-critical efforts. The project has been ongoing for about a year now. This talk will give an overview of current findings and particularly an observation of the current state of the safety-critical ecosystem. - -Particularly, it will share observations on the application of formal methods in the realm right now. - -#### Speaker - -Florian Gilcher is a co-founder of Ferrous Systems and a Rust teacher since 2015. Previously a member of the Rust Community and Core team and a co-founder of the Rust Foundation, Florian is currently focusing to bringing Rust to safety critical systems, such as cars. - -[Video](https://www.youtube.com/watch?v=eaObPhTnoGo) - -### March Meeting (March 28th, 2022) - -Celina Val and Daniel Schwartz-Narbonne will present their work on [Kani](https://github.com/model-checking/kani), a Rust model-checker they are developing at Amazon. - -Kani is a Rust verification tool based on model checking. With Kani, you can ensure that broad classes of problems are absent from your Rust code by writing proof harnesses, which are broadly similar to tests (especially property tests). Kani is especially useful for verifying unsafe code in Rust, where many of the language's usual guarantees can no longer be checked by the compiler. But Kani is also useful for finding panics in safe Rust, and it can check user-defined assertions. - -Kani is currently in the initial development phase, and has not yet made an official release. It is under active development, but it does not yet support all Rust language features." - -https://model-checking.github.io/kani/getting-started.html - -### February Meeting (February 28th, 2022) - -Xavier Denis will discuss [Creusot](https://github.com/xldenis/creusot), his deductive verifier for Rust. Creusot aims to provide efficient verification of complex *safe* Rust code, and is backed by the Why3 verification platform. In this talk we'll briefly cover the high-level architecture of Creusot and some of the unique features in the tool. - -https://www.eventbrite.com/e/creusot-tickets-260072873967 - -### January Meeting (January 31st, 2022) - -Herman Venter gave a retrospective view of his work on [MIRAI](https://github.com/facebookexperimental/mirai), an abstract interpreter for MIR code. We went over key design choices for abstract interpreters and the tradeoffs they imply. - -Find the YouTube video [here](https://www.youtube.com/watch?v=Slf1QWaRe2c). - -### November Meeting (November 29th, 2021) - -[Bas Spitters](twitter.com/basspittersbs) [EventBrite](https://www.eventbrite.com/e/november-meeting-rust-verification-with-bas-spitters-tickets-198474531667). - -**Formal Verification of Subsets of Rust** - -Rust is a big and complex language. Fortunately, it contains a number of interesting sublanguages for which formal verification is more manageable. -I will give an overview of three projects that we are working on in my group. - -[ConCert](https://github.com/AU-COBRA/ConCert) is a Coq framework for reasoning about functional programs, in particular focussing on smart contracts. -As part of this we have developed a general backend to the Coq proof assistant which allows one to generate provably correct functional *rust* programs. -One main use case is to generate rust smart contracts which can be used on the [concordium](https://concordium.com) blockchain. - -[HACSPEC](https://github.com/HACS-workshop/hacspec) is a subset of rust for the specification of high assurance cryptography. We have used it to specify the BLS elliptic curve. This sepcification can be translated to Coq from where we use [fiat-cryptography](https://github.com/mit-plv/fiat-crypto) and [BedRock](https://github.com/mit-plv/bedrock) to generate a correct by construction, efficient, platform independent implementation. - -Find the YouTube video [here](https://www.youtube.com/watch?v=OCehhVDMXKQ). - - -### October Meeting (October 25th, 2021) - -Unfortunately this meeting was not record (my bad). - -We discussed the specifications for a few simple functions in [Prusti](https://github.com/viperproject/prusti-dev) and [Creusot](github.com/xldenis/creusot). -There were quite a few things to say on how we handle borrows and the differences between the two tools. - -A summary will be posted soon. - -The slides are [here](./previous-events/october.pdf) - -### Inaugural Meeting (September 20th, 2021) - -During this meeting, we will introduced the RFMIG, and had a presentation from Vytautas Astraukas of Prusti, showing a little glimpse of verification for Rust software. - -[Youtube recording](https://www.youtube.com/watch?v=ACqgutP0jXs) - -## Previous events - -* [RustVerify2021](https://sites.google.com/view/rustverify2021) -* [RustVerify2020](https://sites.google.com/view/rustverify2020) diff --git a/src/previous-events/october.pdf b/src/previous-events/october.pdf deleted file mode 100644 index 3f21613..0000000 Binary files a/src/previous-events/october.pdf and /dev/null differ diff --git a/src/tools.md b/src/tools.md deleted file mode 100644 index e251249..0000000 --- a/src/tools.md +++ /dev/null @@ -1,73 +0,0 @@ -# Rust verification tools (2021) -This is a list of Rust verification tools with a bias towards ‘formal methods’ tools. An update of Alastair Reid's [2020 list](https://alastairreid.github.io/rust-verification-tools/). -Tool types are listed in approximate (and subjective!) increasing order of the level of expertise required and approximate increasing order of the level of assurance that they provide. General advise on high quality rust can be found in this [book](https://highassurance.rs/). - -## Dynamic checking tools - -* [Miri](https://github.com/rust-lang/miri/) for general UB checking (including data race detection, but only on a single execution) - -### Concurrency checkers -* [Loom](https://github.com/tokio-rs/loom), which focuses on exhaustive checking -* [Shuttle](https://crates.io/crates/shuttle), which focuses on randomized checking - -## Automatic verification tools -Typically relies on a verification harness to generate symbolic input values for the code under test (although those can sometimes be generated from the function argument types). Typically checks assertions, panics, overflows, etc. - -## Bounded model checking / Static Symbolic Execution -* [Kani Rust Verifier](https://github.com/model-checking/kani) -* [SMACK verifier](https://github.com/smackers/smack) -* [Crux-mir](https://crux.galois.com/) [github](https://github.com/GaloisInc/crucible/tree/master/crux-mir) -* [Crust](https://github.com/uwplse/crust) - -## Abstract interpreter ++ -* [MIRAI](https://github.com/facebookexperimental/MIRAI) (also maintains [a page](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/FurtherReading.md) like this) - -## Dynamic Symbolic Execution -* [RVT](https://project-oak.github.io/rust-verification-tools/) -Rust → LLVM → {KLEE,SeaHorn} -Plus a DSL for writing verification harnesses based on the property-based testing library proptest -* [Haybale](https://github.com/PLSysSec/haybale) -symbolic execution engine for LLVM written in Rust -* [Seer](https://github.com/dwrensha/seer) -symbolic execution engine based on Miri (not sure it is active) -* [KLEE-Rust](https://github.com/jawline/klee-rust) -KLEE bindings for Rust (inactive for 6 years) -Unbounded (?) - -## Fully Automated Verification -* [RustHorn](https://github.com/hopv/rust-horn) Automated loop-invariant finding by reduction to CHCs; First proposed the 'prophetic' verification method of Rust - -## Auto-Active Verification -Midway between automatic and interactive verification. Relies on hints/annotations/etc inserted in source code such as function contracts, loop invariants, data structure invariants, etc. - -* [Prusti](https://www.pm.inf.ethz.ch/research/prusti.html) [github link](https://viperproject.github.io/prusti-dev/) -* [Creusot](https://github.com/xldenis/creusot) Rust → whyml verifier; Uses the 'prophetic' verification method - -## Interactive verification -Converts Rust to code in an interactive theorem prover which is then verified with human input. -This allows one to treat more complex programs. - -#### Very safe subset of rust -* [HacSpec](https://github.com/hacspec/hacspec) A specification language for cryptographic primitives in Rust. -Has backends in [F-star](https://www.fstar-lang.org/), [Coq](https://coq.inria.fr/) and [EasyCrypt](https://www.easycrypt.info/). -Also has non-cryptographic applications: [riot bootloader](https://github.com/hacspec/hacspec/blob/master/examples/riot-bootloader/src/lib.rs), the part of the bootloader that selects which image to boot : involves a small hash algorithm and a list traversal. [RIOT link](https://future-proof-iot.github.io/RIOT-fp/events) - -#### Coq -* [ConCert](https://github.com/AU-COBRA/ConCert) extracts functional programs in Coq to Rust by using arenas. It originated from smart contract verification. -* [fiat cryptography](https://github.com/mit-plv/fiat-crypto) is a verified compiler for cryptographic primitives in Coq that generates Rust implementations (and other languages). [WIP](https://github.com/AU-COBRA/AUCurves/blob/main/src/Bedrock/ToRustString.v) on extending bedrock2 with a rust printer. -#### Interactive verification of the foundations of Rust -* [RustBelt](https://plv.mpi-sws.org/rustbelt/) -Semantics close to MIR, focuses on verification of unsafe code, -#### Interactive verification of core subsets of Rust -* [Oxicide](https://github.com/aatxe/oxide), [arxiv link](https://arxiv.org/abs/1903.00982) type systems account of Rust's borrow checker, close to surface rust. -* [WASMCert](https://github.com/WasmCert/WasmCert-Coq) Formalization of the wasm standard -* [VeLLVM](https://github.com/vellvm/vellvm) Formalization of the LLVM compilation infrastructure - -#### LEAN prover - -* [Electrolysis](https://github.com/Kha/electrolysis) Rust → LEAN translator (no longer active, MSc thesis) - -## Standardization/Specification - -* [HacSpec](https://github.com/hacspec/hacspec) A specification language for cryptographic primitives in Rust. -* [Ferrocene](https://ferrous-systems.com/blog/sealed-rust-the-pitch/) (previously called Sealed Rust) diff --git a/src/welcome.md b/src/welcome.md deleted file mode 100644 index 786c0a9..0000000 --- a/src/welcome.md +++ /dev/null @@ -1,28 +0,0 @@ -# Rust Formal Methods Interest Group - -[WG repo](https://github.com/rust-formal-methods/wg) | [Zulip Channel](https://rust-lang.zulipchat.com/#narrow/stream/183875-wg-formal-methods) - -The RFMIG provides a forum for academics, industry users and any other interested party discuss and collaborate on the challenges of Rust program verification. - -Our objectives are to: - -*Improve communication between formal tool developers and the Rust core teams* -- Hold 'office hours' with Rust team members to answer questions about the `rustc` API or the direction of the language. -- Identify weak points in Rust's current tool interfaces, help shepherd the improvements the formal methods community needs. - -*Foster a community of formal methods tools and users* -- Provide a platform for tool developers to share their work and encourage collaboration. -- Gather feedback and input from industrial and hobbyist users of formal method tooling. -- Work towards improving tool inter-compatibility, in particular of specifications. - -## Interesting projects - -These initiatives may interest the developers of formal methods tools for Rust, don't hesitate to join the discussion on Zulip. - -- [Project Stable MIR](https://rust-lang.zulipchat.com/#narrow/stream/320896-project-stable-mir): An effort to define a semi-stable API boundary for the Rust compiler specifically targeting verification usecases. -- [Project Ghost Code](https://rust-lang.zulipchat.com/#narrow/stream/324345-t-lang.2Fghost-code): An experiment to define a generic notion of 'ghost code' for use in the compiler which would enable verification tools to more easily encode their invariants. - -# Upcoming Meetings - -## January (TBA) -s \ No newline at end of file diff --git a/templates/index.html b/templates/index.html new file mode 100644 index 0000000..a12f800 --- /dev/null +++ b/templates/index.html @@ -0,0 +1,73 @@ +{% extends "base.html" %} + +{% block content %} + +

Rust Formal Methods Interest Group

+

The RFMIG provides a forum for academics, industry users and any other interested party discuss and collaborate on the challenges of Rust program verification.

+ +

Our objectives are to:

+ +

Improve communication between formal tool developers and the Rust core teams

+ + +

Foster a community of formal methods tools and users

+ + + + +

Meetings

+ +We host meetings on the last Monday of each month where an invited speaker shares their work on a subject related to formal methods and Rust. The meetings are typically held at 19:00 European time, though the time may be adjusted to accomdate speakers + +{% set meetings_section = get_section(path="meetings/_index.md") %} + +

Upcoming Meetings

+ +{% set curr_time = now()|date(format="%s")|int %} + + +

Past Meetings

+ + + +

Interesting projects

+ +

These initiatives may interest the developers of formal methods tools for Rust, don't hesitate to join the discussion on Zulip.

+ + + +{% endblock content %} diff --git a/templates/shortcodes/meeting_list.html b/templates/shortcodes/meeting_list.html new file mode 100644 index 0000000..e69de29 diff --git a/themes/anemone b/themes/anemone new file mode 160000 index 0000000..a1b6e46 --- /dev/null +++ b/themes/anemone @@ -0,0 +1 @@ +Subproject commit a1b6e4614f68999e325404e670cb7a67de2824a9