Underlying every computing system, from the smallest embedded sensor to the largest warehouse-scale distributed system, ultimately is some form of computing hardware. All software abstractions—from the application logic, to language run-time, operating system, and virtual machine—in the end perform their function through a set of low-level commands to a physical device. This fact provides both significant challenges and opportunities to system security. On one hand, the hardware sub-systems implement the lowest level of computing abstraction and cannot be undercut by software implementation artifacts. By the nature of sitting at this lowest level, hardware mechanisms have the opportunity to provide a formally sound foundation on which to build rich and layered approaches to software security. On the other hand, hardware is physical and attackers are not constrained by the formal model that is used to develop or verify the hardware. Security failures in hardware may not be easily “patched” and may provide complete access to the entire system state.
In this course we will explore recent efforts to bridge “formal methods” techniques to the process of creating and analyzing the next generations of computer processors. In doing so we will explore several different formal technques used in both the context of software and hardware design, and attempt to understand the very edge of both what is possible and what is useful today (with an understanding that those two things are not the same).
Announcements
(Feb 16) Papers for week 6 online
(Feb 1) Note the addition of the "references" tab at the top where we will post some useful papers, tools, and other links
To be prepared for this class one should have a solid background in the basics of computer architecture (including the concepts of caches, branch predictors, assembly language, and elementary digital design), automata theory (including finite state machines, NFAs, regular expressions, and grammars). Background in functional programming, hardware design, and advanced software engineering concepts are helpful but not mandatory. As students in a graduate course, when papers touch upon concepts that one is not familiar with the expectation is that students will take that as an invitation to learn the background necessary to fully understand the work described. Students are expected to come to class having prepared by reading the papers required and participate constructively in discussions.