LowCapsFormally: Low-level Object Capabilities for Formally Watertight Security
To reach this objective, this project takes the perspective that a lowcap assembly language is just another programming language, that can be studied using powerful techniques that are developed for high-level programming languages, particularly logical relations and program logics. Using this methodology, I intend to propose, study and implement novel lowcap security measures and rigorously prove their effectiveness. On the other hand, I also intend to further study effect parametricity: a general property I proposed that formally captured the essence of ocaps. I intend to study and apply it in different contexts: for modular reasoning about ocap and lowcap code, but also in the context of functional and dependently typed programming languages, for a number of different purposes (elaborated below).
This project’s results will range from novel, provably correct security measures built on lowcaps, novel methods for reasoning about such measures, but also novel insights about the nature of ocaps, the relation between object-oriented and functional code and the use of effect parametricity in dependently-typed proof assistants.