Skip to content

Commit cce91c2

Browse files
committed
Update readme
1 parent 104a477 commit cce91c2

1 file changed

Lines changed: 7 additions & 0 deletions

File tree

README.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,12 @@
11
# ![TockOS](http://www.tockos.org/assets/img/tock.svg "TockOS Logo")
22

3+
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.
4+
5+
[![paper]](https://dl.acm.org/doi/epdf/10.1145/3731569.3764856)
6+
7+
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.
8+
9+
310
[![tock-ci](https://github.com/tock/tock/workflows/tock-ci/badge.svg)][tock-ci]
411
[![slack](https://img.shields.io/badge/slack-tockos-informational)][slack]
512
[![book](https://img.shields.io/badge/book-Tock_Book-green)][tock-book]

0 commit comments

Comments
 (0)