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 ( [e-mail]) is a Senior Research Associate in the Department of Computer Science and Technology at the University of Cambridge, U.K.

Robert N.M. Watson ( [e-mail]) is a Senior Lecturer in the Department of Computer Science and Technology at the University of Cambridge, U.K.

Simon W. Moore ( [e-mail]) is Professor of Computer Engineering in the Department of Computer Science and Technology at the University of Cambridge, U.K.

Peter Sewell (Peter. [e-mail]) is Professor of Computer Science in the Department of Computer Science and Technology at the University of Cambridge, U. K.

Peter G. Neumann ( [e-mail]) 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: [e-mail]

June 3–5

SIGSIM-PADS ‘19: SIGSIM Principles of Advanced Discrete Simulation, Chicago, IL, Sponsored: ACM/SIG, Contact: Dong Jin, Email: [e-mail]

June 3–5

S YSTOR ‘19: International Systems and Storage Conference, Haifa, Israel, Sponsored: ACM/SIG, Contact: Moshik Hershcovitch, Email: [e-mail]

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: [e-mail]

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: [e-mail]

June 10–13

ICMR ‘19: International Conference on Multimedia Retrieval, Ottawa, ON, Sponsored: ACM/SIG, Contact: Zhongfei (Mark) Zhang, Email: zhongfei@ cs.binghamton.edu