GEEC All the Way Down
CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST
Pagination or Media Count:
How do we formally verify security properties in today s malleable and evolving Commodity System Software COSS ecosystem Recent advances in applying formal methods to systems software, e.g., IronClad 16 and seL4 19, promise that this vision is not a fool s errand after all. In this position paper we explore the challenges involved in this problem, what research questions the state of the art leaves still open, and our proposal for the next step towards realizing this vision.
- Computer Programming and Software
- Computer Hardware
- Computer Systems