Papers

Reference 1

  • CSpec

    • Reference 1 201901 note. Verifying concurrent software using movers in CSPEC. OSDI, 2018. ↩

  • 2019 Arm Os

    • Reference 1 Scalable Translation Validation of Unverified Legacy OS Code. FMCAD, 2019. ↩

  • Intscope

    • Reference 1 Decompiler: Bestar, IDA Pro as front-end. translates x86 assembl into PANDA IR (freshly designed). Symbolic execution engine: leverage framework of GiNac[^c8]. Path Validator and Integer Overflow Checker: STP, a decision procedure for bit-vectors and arrays. Evaluation 20 zero-day integer overflows in QEMU, Xen, Xine, MPlayer, VLC. [^c8] IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution. NDSS. 2009. ↩

  1. reference ↩
Created Oct 30, 2019 // Last Updated May 18, 2021

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

... what would you change?