Reference:
References: reference More uCFI References: Enforcing Unique Code Target Property for Control-Flow Integrity, CCS’18 UCT: Unique Code Target ICT: Indirect Control-flow Transfer Key: collecting the necessary runtime information and using it to augment the points-to analysis on control data. Contraining data: the data helps to determine the target of indirect calls. How to identify the constraining data? How to collect this data efficiently? How to perform the points-to analysis efficiently and accurately?
Reference 1 Capability Reference 1 ACL vs Capability Access control list: attributes on objects, stating which subjects has which permissions; e.g. file permission attribute bits on Linux. Capability: attributes on subjects, stating the subject has what permissions over certain objects; format, each capability has form of ; a subject can have a list of capabilities. reference ↩ Confused Deputy References: N. Hardy, “The confused deputy (or why capabilities might have been invented),” ACM SIGOPS Operating Systems Review, vol.
Reference 1 Cves Reference 1 Two CVEs on FreeRTOS: reference ↩ reference ↩
Reference: ARMor: Fully Verified Software Fault Isolation Published at EMSOFT’11. Reference:
Paper1: Make software immune to observation and modification. Tamper-resistance using Integrity Verification Kernels: segments of code which are self-modifying, self-decrypting and installation unique. code segments communicates with other such code, creating an interlocking trust model. Threats: breach communication access controls to attack the system; computer virus; attacker as insider: may modify at will. Tamper Resistant Software Design and Implementation. 1999. ↩
Reference: 2009 Micro Cfo Reference 1 Deferred exception Itanium: deferred exception tracking. can be used to support for information flow tracking. Deferred exception for speculatively executed instructions. An exception is deferred for later handling instead of being thrown out immediately. Each general purpose register is extended with an additional deferred exception token (NaT, Not a Thing) to keep track of exceptions. Token is propagated along with the executing instructions.
References: reference More sel4: time protection 2020 Carrv Wistoff: Prevention of microarchitectural covert channels on an open-source 64-bit risc-v core References: Wistoff, Nils, Moritz Schneider, Frank K. Gürkaynak, Luca Benini, and Gernot Heiser. “Prevention of microarchitectural covert channels on an open-source 64-bit risc-v core.” arXiv preprint arXiv:2005.02193 (2020). fence.t Temporal Fence Instruction fence.t More
References: PSOS CompCert seL4 CertiKOS More PSOS The Provably Secure Operating System (PSOS) project began in 1973 and continued until 1983. The 1980 PSOS final report includes the system architecture and many of the basic hardware and operating system layers, plus some illustrative applications (all formal specified in the SPECIAL language of HDM, the Hierarchical Development Methodology). The Feiertag/Neumann paper summarizing the architecture as of 1979 is available in a retyped, more or less correct, hand-edited pdf form.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?