Towards formally verified compilation of tag-based policy enforcement
Towards formally verified compilation of tag-based policy enforcement
复制标题
实现基于标签的策略执行的正式验证编译
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
S. Anderson
中科院分区：
文献类型：
--
作者：
Chr Chhak;A. Tolmach;S. Anderson
硬件辅助参考监测作为一种改进现有软件安全性的方法正受到越来越多的关注。一个例子是PIPE体系结构扩展，它将元数据标记附加到寄存器和内存值上，并在每条机器指令上执行基于标记的规则，以强制执行软件定义的安全策略。为了有效地使用PIPE，工程师应该能够根据源级概念（如函数、局部变量和结构化控制操作符）编写安全策略，这些概念在机器级别是不可见的。编译器的工作是生成能够感知管道的机器代码，以执行这些源代码级策略。编译器因此成为被监视系统的可信计算基础的一部分——因此是验证的主要候选者。为了在此设置中形式化编译器的正确性，我们使用自己的用户指定的基于标记的监视形式扩展源语言语义，并显示编译器保留该监视行为。编译的挑战包括将源级监视策略映射到指令级标记规则，保留故障停止行为，以及满足传统优化的复杂前提条件。在本文中，我们描述了Tagine的设计和验证，Tagine是一个小型原型编译器，可以将简单的带标签的WHILE语言转换为带标签的寄存器传输语言并执行简单的优化。Tagine基于CompCert编译器的RTLgen和Deadcode阶段，因此是用Coq编写和验证的。这项工作是验证实际标记源语言的全面编译器的第一步。
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 work is a first step toward verification of a full-scale compiler for a realistic tagged source language.