Explores techniques for robust system construction in the face of complexity, drawing from work in microprocessor architecture, transaction processing, operating systems, formal specification and verification, and practical experience. We will look fairly carefully at various applications of dataflow driven computation and rollback strategies and how these ideas have been applied in the context of microkernel-based operating systems. We will examine the performance implications of these techniques, and their implications for security and predictable latency. Finally, we will examine the relevance of these techniques to formal verification of overall correctness invariants.

Explores various issues in operating system security, ranging from formal results and their significance to examining real high-security implementations. We will briefly examine covert timing and storage channels, with an eye toward understanding their implications for operating system architecture. Finally, we will look at current operating system research efforts here at Hopkins and how these issues are being addressed. Students will be expected to complete a significant project.