From cce91c250a9501ed2675c6d975ce77444cce90f2 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Wed, 18 Feb 2026 13:25:10 -0800 Subject: [PATCH 1/2] Update readme --- README.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/README.md b/README.md index 095c70df79..4e42939bc6 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,12 @@ # ![TockOS](http://www.tockos.org/assets/img/tock.svg "TockOS Logo") +This repository contains TickTock-a fork of the Tock OS that verifies memory isolation for user space processes. [Flux](https://github.com/flux-rs/flux) is used for the verification. + +[![paper]](https://dl.acm.org/doi/epdf/10.1145/3731569.3764856) + +The main verification bits can be found under the `kernel` directory, along with the arch directory. Specifically, `allocator.rs` contains the memory allocator referenced in the paper. `arch/cortex-m/src/mpu.rs` contains the MPU implementation for ARMv6m and ARMv7m devices. `arch/rv32i/src/pmp.rs` contains the MPU implementation for RISC devices. + + [![tock-ci](https://github.com/tock/tock/workflows/tock-ci/badge.svg)][tock-ci] [![slack](https://img.shields.io/badge/slack-tockos-informational)][slack] [![book](https://img.shields.io/badge/book-Tock_Book-green)][tock-book] From 23fda53831177be188adce57572c9970b0cf4dc0 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Wed, 18 Feb 2026 13:30:39 -0800 Subject: [PATCH 2/2] Update readme --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 4e42939bc6..6c151481d3 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,7 @@ This repository contains TickTock-a fork of the Tock OS that verifies memory iso The main verification bits can be found under the `kernel` directory, along with the arch directory. Specifically, `allocator.rs` contains the memory allocator referenced in the paper. `arch/cortex-m/src/mpu.rs` contains the MPU implementation for ARMv6m and ARMv7m devices. `arch/rv32i/src/pmp.rs` contains the MPU implementation for RISC devices. +You can find Lean proofs for SMT solver issues in this [repo](https://github.com/PLSysSec/vtock-lean). Verification of the ARM interrupt handlers and context switching code can be found in this [repo](https://github.com/PLSysSec/tock-veri-asm). [![tock-ci](https://github.com/tock/tock/workflows/tock-ci/badge.svg)][tock-ci] [![slack](https://img.shields.io/badge/slack-tockos-informational)][slack]