Towards Formally Verified Compilation of Tag-Based Policy Enforcement

CHR Chhak, Andrew Tolmach, Sean Anderson

Hardware-assisted reference monitoring is receiving increasing attention as a way to improve the security of existing software. One example is the PIPE architecture extension, whic…