KTH STEP group

Secure and Trustworthy Execution Platforms @ KTH

KTH

Pinned Repositories

EmbExp-Box_firmware
Language:C4 3 10
EmbExp-ProgPlatform
Embedded Experiments - the program platform
Language:C1 2 13
HOL4P4
P4 formalization using Ott and HOL4
Language:Standard ML10 5 10
HolBA
Binary analysis in HOL
Language:Standard ML36 4 4921
itppv-course
Interactive Theorem Proving course using HOL4
Language:Standard ML10 5 00
mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Language:Standard ML2 4 00
p4ott_syntax
Language:Standard ML1 4 00
s3k
Capability based separation Kernel for embedded RISC-V.
Language:C5 4 22
s3k-poc
Proof-of-concept application using the S3K kernel
Language:C1 4 00
separation-kernel
Language:C2 4 00

KTH STEP group's Repositories

kth-step/HolBA
Binary analysis in HOL
Language:Standard ML36 4 4921
kth-step/HOL4P4
P4 formalization using Ott and HOL4
Language:Standard ML10 5 10
kth-step/itppv-course
Interactive Theorem Proving course using HOL4
Language:Standard ML10 5 00
kth-step/s3k
Capability based separation Kernel for embedded RISC-V.
Language:C5 4 22
kth-step/EmbExp-Box_firmware
Language:C4 3 10
kth-step/mil
Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML
Language:Standard ML2 4 00
kth-step/separation-kernel
Language:C2 4 00
kth-step/dma-controller-verification
Language:Standard ML1 4 00
kth-step/EmbExp-ProgPlatform
Embedded Experiments - the program platform
Language:C1 2 13
kth-step/fp-course
1 5 00
kth-step/p4ott_syntax
Language:Standard ML1 4 00
kth-step/s3k-poc
Proof-of-concept application using the S3K kernel
Language:C1 4 00
kth-step/Silver-Pi
Verified Pipelined Processor Circuit
Language:Standard ML1 4 01
kth-step/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
Language:Standard ML0 3 00
kth-step/HolBA-multicore
Binary analysis in HOL
Language:Standard ML0 2 00
kth-step/Hypervisor
Language:C0 4 00
kth-step/probability-jam
We collect theory files and references for learning probability theory with HOL4.
Language:Standard ML0 4 00
kth-step/abs-metatheory
Language:Coq5 6
kth-step/BIR-angr
Language:Python1
kth-step/EmbExp-BalRob
Embedded Experiments - balancing robot demo
Language:C2 0
kth-step/EmbExp-Box
Language:Python3 52
kth-step/EmbExp-Logs
Language:Python4 02
kth-step/evoting-demonstrator
Language:C
kth-step/hypervisor.linux
Language:C4 0
kth-step/kth-step.github.io
KTH STEP group's website
Language:SCSS3 01
kth-step/libs3k
User-space library for S3K.
Language:C
kth-step/s3k-examples
Language:Meson
kth-step/sw-spi-cam-model
Language:Standard ML4 1
kth-step/syntax-course
Code and other material related to a course in Swedish on formal languages and syntax analysis
Language:Java
kth-step/VM_SCAMV_intro
Language:Shell4 0