specific security properties. We believe
this CHERI system architecture has
significant potential to provide unprecedented total-system trustworthiness,
including addressing some of the side-channel attacks that were unknown at
the time of its conception.
19
Such architectural guarantees enable
more secure implementation of currently
insecure languages (such as C/C++) and
can put demonstrably secure operating-system kernels on a more secure
foundation. Similar approaches may
apply in other domains, for example
between vulnerable components
across a system-on-chip.
Engineering such systems requires a more holistic view, with a
tighter interplay between hardware,
operating systems and applications.
In particular, designers need to understand more of what takes place
in layers above or below their field of
expertise. Better architectural models
enable more robust verification of security properties, and amortizing verification costs across projects helps
defenders but not attackers. Such
verification must be inclusive, testing
all the aspects of a system including
the boundaries of implementation-defined behavior.
Better verification can defend us
against new vulnerabilities present in
the abstractions it is based upon, but
not against those that involve phenomena that are not modeled. An open
question is whether there is an abstraction between an architectural specification and a full hardware implementation that allows us to fully reason
about potential leakage, without being
so complex as to being intractable.
Conclusion
Traditional models—in which designers have free reign within tightly constrained layers—are no longer fit for
purpose. Hardware/software system
security architects need better awareness of what comes above and below
them, to be able to reason about what
happens at other levels of abstraction,
and to understand the effects of composition. Managing overall complexity must fully capture information that
might be relevant for security analysis,
especially for entirely new classes of
vulnerabilities. The defensive battle
has only just begun.
References
1. Armstrong, A. et al. ISA Semantics for ARMv8-A,
RISC-V, and CHERI-MIPS. In Proceedings of the
Principles of Programming Languages Conference
(POPL) 2019.
2. Bangert, J. et al. The page-fault weird machine:
Lessons in instruction-less computation. In
Proceedings of the USENIX Workshop on Offensive
Technologies (WOOT), 2013.
3. Bellovin, S. M. and Neumann, P. G. The big picture: A
systems-oriented view of trustworthiness. Commun.
ACM 61, 11 (Nov. 2018), 24–26.
4. Beniamini, G. Over The Air: Exploiting Broadcom’s Wi-Fi
Stack; https://bit.ly/2oA6GJL
5. Gerber, S. et al. Not your parents’ physical address
space. In Proceedings of the Hot Topics in Operating
Systems Conference (HotOS-XV) 2015.
6. Goel, S., Hunt, W.A. Jr., and Kaufmann, M. Engineering
a formal, executable x86 ISA simulator for software
verification. Provably Correct Systems (ProCoS), 2017.
7. Google Project Zero, 2018; https://bit.
ly/2CAQz TMGu, R. et al. CertiKOS: An Extensible
Architecture for Building Certified Concurrent OS
Kernels. OSDI 2016, 653–669; See also https://bit.
ly/2Uzj9sI for ongoing work.
8. Islam, S. et al. SPOILER: Speculative Load Hazards
Boost Rowhammer and Cache Attacks, arXiv e-prints
(Mar. 1, 2019); https://bit.ly/2Tx Wdhk
9. Klein, G. et al. Comprehensive formal verification of
an OS microkernel. ACM Trans. Computer Systems
2014; See also https://bit.ly/2UPKgE Y for ongoing
work.
10. Kocher, P. et al. Spectre attacks: Exploiting
speculative execution. ArXiv e-prints (Jan. 2018);
https://bit.ly/2lUpJLk
11. Leroy, X. A formally verified compiler back-end. Journal
of Automated Reasoning 43, 4 (2009), 363–446.
12. Lipp, M. et al. Meltdown, 2018; https://bit.ly/2E6my Yl
13. Markettos, A. T. Making sense of the Supermicro
motherboard attack; https://bit.ly/2PqOnld
14. Markettos, A. T. et al. Thunderclap: Exploring
vulnerabilities in operating system IOMMU protection
via DMA from untrustworthy peripherals. In
Proceedings of the Network and Distributed Systems
Security Symposium (NDSS), (Feb. 2019).
15. Rushanan, M. and Checkoway, S. Run-DMA. In
Proceedings of the WOOT 2015 Conference. (2015).
16. Sutherland, G. Secrets of the motherboard ([sh*t]
my chipset says). In Proceedings of the 44CON 2017,
(Sept. 2017).
17. Van Bulck, J. et al. Foreshadow: Extracting the keys
to the Intel SGX kingdom with transient out-of-order
execution. USENIX Security (Aug. 15–17, 2018);
https://bit.ly/2DusEDT
18. Watson, R.N.M. et al. Capability Hardware Enhanced
RISC Instructions (CHERI): Notes on the Meltdown
and Spectre Attacks. Technical Report UCAM-CL- TR-916, University of Cambridge, Computer
Laboratory (Feb. 2018); https://bit.ly/2DuVDrr
19. Watson, R.N.M. et al. Capability Hardware Enhanced
RISC Instructions (CHERI): CHERI Instruction-set
Architecture, Version 7, Technical Report UCAM-CL- TR-927, University of Cambridge, Computer
Laboratory (Apr. 2019); https://bit.ly/2XzPgKU
20. Weisse, O. et al. Foreshadow-NG: Breaking the virtual
memory abstraction with transient out-of-order
execution (Aug. 2018); https://bit.ly/2VZLD0h
A. Theodore Markettos ( theo.markettos@cl.cam.ac.uk)
is a Senior Research Associate in the Department of
Computer Science and Technology at the University of
Cambridge, U.K.
Robert N.M. Watson ( robert.watson@cl.cam.ac.uk) is a
Senior Lecturer in the Department of Computer Science
and Technology at the University of Cambridge, U.K.
Simon W. Moore ( simon.moore@cl.cam.ac.uk) is
Professor of Computer Engineering in the Department of
Computer Science and Technology at the University of
Cambridge, U.K.
Peter Sewell (Peter. Sewell@cl.cam.ac.uk) is
Professor of Computer Science in the Department of
Computer Science and Technology at the University of
Cambridge, U. K.
Peter G. Neumann ( neumann@csl.sri.com) is Chief
Scientist of the SRI International Computer Science Lab,
and moderator of the ACM Risks Forum.
Copyright held by authors.
Calendar
of Events
June 2–6
JCDL ‘19: The 18th ACM/IEEE
Joint Conference on Digital
Libraries Champaign, IL,
Sponsored: ACM/SIG,
Contact: J. Stephen Downie,
Email: jdownie@illinois.edu
June 3–5
SIGSIM-PADS ‘19:
SIGSIM Principles of Advanced
Discrete Simulation,
Chicago, IL,
Sponsored: ACM/SIG,
Contact: Dong Jin,
Email: dong.jin@iit.edu
June 3–5
S YSTOR ‘19: International
Systems and Storage Conference,
Haifa, Israel,
Sponsored: ACM/SIG,
Contact: Moshik Hershcovitch,
Email: moshikh@il.ibm.com
June 3–6
SACMAT ‘19: The 24th ACM
Symposium on Access Control
Models and Technologies,
Toronto, ON,
Sponsored: ACM/SIG,
Contact: Atefeh (Atty) Mashatan,
Email: amashatan@ryerson.ca
June 5–7
TVX ‘19: ACM International
Conference on Interactive
Experiences for TV and
Online Video,
Salford (Manchester), U.K.,
Sponsored: ACM/SIG,
Contact: Jonathan Hook,
Email: jonathan.hook@york.
ac.uk
June 9–12
UMAP ‘19: 27th Conference on
User Modeling, Adaptation
and Personalization,
Larnaca, Cyprus,
Co-Sponsored: ACM/SIG,
Contact: George Angelos
Papadopoulos,
Email: george@cs.ucy.ac.cy
June 10–13
ICMR ‘19: International
Conference on Multimedia
Retrieval,
Ottawa, ON,
Sponsored: ACM/SIG,
Contact: Zhongfei (Mark) Zhang,
Email: zhongfei@
cs.binghamton.edu