Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 19:15 - 19:30 at CPP - Security, Blockchains, and Smart Contracts Chair(s): Andreas Lochbihler

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, which attaches metadata tags to register and memory values and executes tag-based rules at each machine instruction to enforce a software-defined security policy. To use PIPE effectively, engineers should be able to write security policies in terms of source-level concepts like functions, local variables, and structured control operators, which are not visible at machine level. It is the job of the compiler to generate PIPE-aware machine code that enforces these source-level policies. The compiler thus becomes part of the monitored system’s trusted computing base — and hence a prime candidate for verification.

To formalize compiler correctness in this setting, we extend the source language semantics with its own form of user-specified tag-based monitoring, and show that the compiler preserves that monitoring behavior. The challenges of compilation include mapping source-level monitoring policies to instruction-level tag rules, preserving fail-stop behaviors, and satisfying the surprisingly complex preconditions for conventional optimizations. In this paper, we describe the design and verification of Tagine, a small prototype compiler that translates a simple tagged WHILE language to a tagged register transfer language and performs simple optimizations. Tagine is based on the RTLgen and Deadcode phases of the CompCert compiler, and hence is written and verified in Coq. This is a first step toward verification of a full-scale compiler for a realistic tagged source language.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30: Security, Blockchains, and Smart ContractsCPP at CPP
Chair(s): Andreas LochbihlerDigital Asset

Streamed session: https://youtu.be/Qak5mK92etU?t=2832

18:45 - 19:00
Talk
Extracting Smart Contracts Tested and Verified in Coq
CPP
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Mikkel MiloConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
Pre-print Media Attached File Attached
19:00 - 19:15
Talk
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
CPP
Victor Cacciari MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity of Minho, Guy L. Steele Jr.Oracle Labs
Pre-print Media Attached
19:15 - 19:30
Talk
Towards formally verified compilation of tag-based policy enforcement
CPP
CHR ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State University
Pre-print Media Attached