Arch


Ongoing (as of 2022-03-28)

  • Formal Verification in EDA
    • theory: the book
    • practice: ?
  • Formal Verification in OS(SeL4)
    • theory: the paper; methodology/workflow/tools;
    • practice: sel4 testing/verification code examples; test run;
  • Architectural design in SonicBoom/C910
    • theory: pipeline/cache/mem design
    • practice: read code examples; test run;

Reference:

  • Basics
  • Reference 1 Two Types of Logic Blocks Combinational Logic Blocks without memory are called combinational; the output of a combinational block depends only on the current input. Can be defined by truth table, boolean algebra. Decoders: n-bit input -> 2^n outputs Multiplexors: a selector: output is one of the inputs that is selected by a control. Sequential Logic Sequential logic is logic including state. In blocks with memory, the outputs can depends on both the inputs and the value stored in memory, which is called the state of the logic block.

  • Secure Virtual Architecture
  • Todos Where is the pool metadata created/used in SAFECode passes? Where is the runtime check instrumentation in SAFECode passes? Learn the code from SVA on FreeBSD and propose a solution for the policy to be ported/re-implemented on CheriBSD: sosp 2007 booting signal handler dispatch code I/O instructions. kernel allocators. for analysis(ch6.3): int to pointer casts, stack usage, sys_iotctl, initial task structure, stack pointer to structure. sec 2009

  • Pump
  • Q&A How to init tags? LLM: developer writes rules in a special language; software handler computes the rule and generates mappings of tags (as policy) 2018sp-stack: Compiler + adding instructions into programs. 2018sp-stack: Lazy tagging (first write) + Lazy clearing (on all write, check only on read) How to propagate tags? LLM: mapping of tags (policy rules) will be used to propagagte tags during execution of PUMP.

  • Neverland
  • Reference 1 Neverland: Lightweight Hardware Extensions for Enforcing Operating System Integrity. Montivations Current solutions has draw backs: Secure Boot, driver signing Secure Boot is not enough to protect kernel from being tempered: attackers could exploit software vulnerabilities to perform malicious actions such as overwriting kernel memory, executing malware in kernel-mode, or disabling driver integrity checks (example attacks can be seen in [^c64] [^c8] [^c16] [^c41] [^c62] [^c54] [^c48] [^c44]).

  • Secure TLBs
  • Reference 1 Secure TLBs. ISCA, 2019. ↩

  • AI Chips
  • References: AI Chips: What They Are and Why They Matter. Saif M. Khan, April 2020. General-purpose Chips (CPU) vs. Specialized Chips (GPU, FPGA, ASIC) Different types of AI chips are useful for different tasks. GPUs are most often used for initially developing and refining AI algorithms; This process is known as “training”. FPGAs are mostly used to apply trained AI algorithms to real-world data inputs; This is often called “inference”.

  • Fpga
  • References: reference FPGA vs ASIC CBB: Common Building Block. Timing Constraints: Tsu: Time of Set up Th: Time of Hold SDC: Synopsys Design Constraints STA: Static Timing Analysis More

  • Vivado Usage Tips
  • Out of date One can ‘force up to date’ if changes are detected by vivado but those changes can be ignored (unrelated to the regarding operation). Out of date – force up to date Out of Context Modules Vivado IP的两种综合方式:Global 和 Out-Of-Context More

  • Rtl Verification
  • References: reference More UVM - Universal Verification Methodology References: UVM shizhan, juan I IC design process design: Verilog/VHDL verification: Verilog, SystemVerilog, SystemC, More

Created Jul 30, 2019 // Last Updated Oct 8, 2022

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

... what would you change?