References:
IC/ASIC adoption trends for formal property checking (e.g., model checking), as well as automatic formal applications:
References: Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. By Mohammad Rahmani Fadiheh, et. al. 2018 arXiv, 2019 DATE UPEC: Unique Program Execution Checking. Orc Attack Leverage the RAW(Read after write) hazard: load latency is longer when RAW happens. Assumptions: (simplified for easy understanding) each cache line is selected based on lower 8 bits; a total of $2^8=256$ cache lines. Attack: guess a possible address #test_value; write a value at the #test_value load a secret to a register lw x4, 0(x1), where x1 is #protected_addr; ==> this will throw an exception, x4 will not have the secret value (not architectual visible).
References: Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, 2017, ICFP Wednesday @ 1130, 2016. Kami A Framework for RISC V HW Verification Murali Vijayaraghavan, MIT More
References: Relaxed-Memory Concurrency x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors Relaxed-Memory Concurrency Multiprocessors are now pervasive and concurrent programming is becoming mainstream, but typical multiprocessors (x86, Sparc, Power, ARM, Itanium) and programming languages (C, C++, Java) do not provide the sequentially consistent shared memory that has been assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, exposing behaviour that arises from hardware and compiler optimisations to the programmer.
References: reference EDA languages PSL: Property specification language (EDA standard) evovled from Sugar language; adopted as an IEEE standard (1850-2010); grafted onto both SystemVerilog and VHDL; act as an add-on to SystemVerilog/VHDL; Based on CTL/LTL; PSL is divided into four layers: Boolean layer (lowest layer), consists of instantaneous boolean expressions on signals in the design under test; The syntax of this layer follows that of the HDL to which PSL is being applied; Can be verilog, SystemVerilog, VHDL, or others; e.
References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. Chaper 15-20 More Logic Verification -- languages References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. Chaper 15 Steps of IC design design in C/C++ model –> simulators, func good design in RTL –> simulating, and compare with the C/C++ reference model Synthesis: Translate RTL to gate-level netlist.
References: RISCV Sail on Github Using Sail Specifications in Isabelle/HOL, August 29, 2018. pdf Sail Goals: engineer-friendly, vendor-pseudocode-like language for describing instruction semantics. Sail: a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths. Side-effects: Sail use its effect system to determine whether a function has side-effects and needs to be monadic. Monadic function: All about monads: Monads is a way to structure computations in terms of values and sequences of computations using typed values.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?