CHERI
- Introduction
  - Motivations
- Cheri C Model
  - Provenance
  - DepthOfC
    - Undef
- Cheri Temporal
  - MICRO'19 CHERIvoke
  - SP20 Cornucopia
- Cheri Spatial
- Cheri Domain
- CheriABI
- Cheri Concentrate
- CheriBSD
- Cheri FreeRTOS
- Cheri RTOS
- Cheri Hypervisor
- Cheri Cloud
- Cheri Formal
  - 2019 Rigorous
- Cheri Link
- CHERI ISA
  - Regs
    - Specialregs
  - Sail Desc
  - Instructions
    - Csc
    - CGet/SetDefault
  - InstEncode
    - Cap Mode
  - CHERIoT
- Cheri Tag
- Cheri ELF
- BERI
  - Piccolo
  - Flute
  - Beri Isa
  - Cheri
    - MIPSTop.bsv
    - Example CSC
    - Writeback
    - MIPS.bsv
    - ICache
    - Test
    - tagsparams.py
    - Expand Bits
    - Tag Lookup
    - MultiLevelTagLookup.bsv
    - Master Slave
    - L2Cache
    - Merge.bsv
    - CacheCore.bsv
    - CP0
    - MemTypes.bsv
      - Data
    - Tag Controller
    - DCache.bsv
    - TLB
    - TagCache.bsv
    - Memory.bsv
    - Execute.bsv
    - CoProConversionFunctions.bsv
    - Scheduler.bsv
    - MemAccess.bsv
    - CapCop.bsv
- Cheri X86
- CHERI ARM
- CHERI RISC-V
- CHERI MIPS
- Cheri Qemu
  - Translate
  - Addr Trans
  - Inst Fetch
  - Guest RAM
    - Code
  - Memtrace
    - Simple
  - Tag Mem
  - Cheriops
    - CLoadTags
  - Basics
  - Build
- Cheri LLVM
- Hacking
  - Cross
    - Cheribuild
  - Sandbox_user
  - Hello
- Security
- Cheri-CFI
Privilege Separation
Program Analysis
System Security
- Security Policies
  - Bell-LaPadula
- Attacks
  - Sgx
  - Rop
  - Container PE
  - DOP
  - Side Channel
    - Spectres
- Defences
  - Control Flow
    - uCFI
  - Capability
    - Capability
    - Confused Deputy
  - Silhouette
    - Cves
  - Sfi
    - ARMor
  - Tamper Resistance
  - Info Flow
    - 2009 Micro Cfo
    - Lattice
  - Side Channel
    - 2020-RISCV
  - Verified
    - PSOS
    - Certikos
- Detection
  - Hw Monitor
  - Prima
  - Flicker
  - VerifyExe
- VMI
  - Hwvmi
    - 2016 Flexcore
- Surveys
  - 2020 Iot Sec
Memory Safety
- Temporal
- Mem Tag
- Pagebits
  - Dang
  - HyperSafe
  - Intel MPK
- Sec Compile
  - 201904 Secswift
  - Sok Stack
  - HW-stack
  - Translator
  - EPOXY
  - Minion
  - nesCheck
  - uXOM
  - Rest
  - Safemem
  - Asan
    - Califorms
- Ptr Meta
  - Cpi
    - 2014 OSDI CPI
  - Tagged Pointer
    - 2021 In-Fat Pointers
  - Ptr Auth
  - Runtime Check
    - Jones Kelly
    - Ruwas Lam
  - 2010 CETS
    - Runtime
  - LowFat
  - PLDI'09 SoftBound
  - HardBound
  - M-Mmachine
  - Intel MPX
  - Intel Ccc
- Seclang
  - CCured
  - nesC
- Attacks
- RIPE
OS
- Basics
- Unikernels
  - Demikernel
- Freertos
- L4
  - seL4
- OS in Rust
- Gnu Hurd
- Freebsd
  - jemalloc
  - Vm
    - Page Fault
  - AST
  - vnode
  - Boot
  - Sysinit
  - IDT
  - VG-Code
  - Unrhdr
  - cpu_switch
- Minix 3
- Linux
  - Page Table
  - execve
- Windows
  - Heap Protection
Compilers
- Basics
- Verify
  - Sec Gap
  - Next700
  - CompCert
  - Binary Verify
  - 1967
    - 1962
- LLVM
  - Exceptions
    - Landingpad
  - New Pass
  - Table Gen
  - Debug Info
    - DIExpression
  - Naming
  - LTO
  - Extending
  - Metadata
  - Tools
    - Regression Tests
      - Cheri
  - Asm
    - Mc Toll
    - Remill
    - McSema
    - S2e
    - Revgen
  - Proj
  - Hacking
    - Types
  - Attr
  - Addrspace
  - Instvisitor
  - IR
  - Data Layout
- Auto Parallel
CodeGen
- Relocations
- lld
- Prolog Epilog
  - Mips
- Core ISel
- Stack Frame
- ELF in OS
  - Loading
    - Init
    - Freebsd
  - Relocation
    - RELRO
  - Text
  - .debug
  - .symtab
  - Global
- Call Conv
- Linkers Loaders
  - Linker Scripts
- MC
- MIR
  - MachineFunctionPass
- Reg Alloc
- Basics-Asm
- Backend-Cpu0
Arch
- Basics
  - Gem5
    - Trace Cpu
    - MemMap
    - Stats
    - Traffic Gen
    - Memobj
    - Extending
    - Fs
    - Ruby
    - O3 CPU
    - ArchSupports
    - Gem5 KVM
  - ECE401/201 Adv
  - Arm
    - Trustzone
    - VMSA(AArch64)
  - X86
  - Mips
    - CP0
      - Regs
    - Instructions
    - Regs
  - RISC-V
    - Attacks
      - SP-Analog
    - Ibex
    - Sonic Boom
    - J Ext
    - Iopmp
  - Bluespec
    - Packages
      - Connectable
        
        Get Put
        
        Client Server
    - Types
    - Type Classes
    - Modules
    - Tlm
  - Systemv
    - Verilog
  - C910
  - Chisel
- SVA
  - PoolAlloc
  - SAFECode
    - Control-C
    - 2003 NoGC
    - 2005Embed
    - Steensgaard
    - Type System
    - Runtime Checks
      - Function Ptrs
      - Arraychecks
    - Passes
  - LLVA OS
  - SVA-OS
  - HW/SW
    - Secure Interface
    - KCoFI
  - VGhost
    - .svamem
  - Intrinsics
  - Intrumentation
- Pump
- Neverland
- Secure TLB
- AI Chips
- Fpga
- Vivado
- RTL-V
  - UVM
Languages
- Closure
- Lambda
  - Lambda Lifting
- Langs
  - Sequoia
  - C & C++
    - Mesh
  - NesC
  - Go
    - Setup
    - Tour
  - Rust
    - Oxide
  - ProofCC
  - Ada
  - C
- Tensors
- Mix Langs
  - Fun Tal
- Tapl
  - Semantic Style
- Aop
- Class PLDI
- TAL
- Types
Parallel
- Consistency
Logics
- Software Fundations
  - V1 LF
    - Coq
  - V2 PLF
  - V3 VFA
  - V4 QC
  - V5 VC
- Concrete Semantics
- Modern89
  - Logic Methods
- FM
  - Basic Concepts
    - Monads
  - Constructive Logic
  - Abstract Algebra
    - Groups
  - Galois
  - Abs Int
  - Papers
  - Temporal Logic
    - CTL
  - MC
  - Hott
    - Intro
  - Separation Logic
- Fm in Arch
  - UPEC
  - Kami
  - Spec Hol4
  - Spec Psl
  - EDA FM
  - Spec Sail
    - Islaris-ARM
    - RISCV Sail
- Tools
  - Kami
  - Coq
  - Isabelle
  - SCADE
  - Z3
- Class Logic
- Class Math220
IOT
- AI
- 5g
- Env
  - ALeaves
- Batteryless
- Edge
  - Migration
AI
Cert
- Asil
- Cc
- Psa
- 26262
Books
- Shelf
- Formal Methods
Practice
- Linux
  - Lubuntu
- Tools
  - Mscode
  - Vim
  - Make
  - Gdb
  - Rsync
  - Cscope/Vim
  - Git
- 编程之美
- Book CNSPP
- Coding
  - 错误笔记
  - Dyn
    - Knapsack
Research
- Bios
  - Margo Seltzer
- Reading
- Seminars
- Paper Writing
  - Limitations
- Conferences
  - EdgeIoT
- Job Choices
教育
- CS.EDU

Clear History

Built with from Grav and Hugo

Welcome > Logics > Tools/Methods > Kami

Kami

References

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Kami: A Framework for (RISC-V)HW Verification

Created Jul 15, 2020 // Last Updated Nov 7, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?