PARseL：面向基于seL4的已验证信任根

嵌入式/IoT/CPS设备的广泛采用与日益增长的热度，使其成为极具吸引力的攻击目标。在中低端设备上，受各类约束所限，安全特性通常很少甚至没有。此类设备因此易遭受基于恶意软件的入侵。一种流行的防御措施是远程证明（RA），其允许可信实体确定不可信远程设备当前的软件完整性。对于高端设备，RA可通过安全硬件组件实现。对于低端（裸机）设备，极简混合（硬件/软件）RA行之有效，但会带来一些硬件改动。这就留下了某些配备标准硬件组件（例如内存管理单元（MMU）以及可能的安全启动机制）的中端设备（如ARM Cortex-A系列）。在这一领域中，seL4（具有保证进程隔离的已验证微内核）是实现RA的一个有前景的平台。HYDRA朝此方向迈出了第一步，尽管未实现任何可验证性或可证明保证。本文承接HYDRA未竟之处，构建了一种PARseL架构，将全部用户依赖组件与TCB分离。这基于seL4本身带来了更强的隔离保证，并便于形式化验证。在PARseL中，我们使用形式化验证为隔离的RA TCB获取若干安全属性，包括：内存安全、功能正确性与秘密独立性。我们在F*中实现PARseL，并使用霍尔逻辑指定/证明预期属性。接下来，我们利用KaRaMeL将F*实现自动翻译为C，从而保留PARseL C实现（位于seL4之上）的已验证属性。最后，我们在一台商用平台——SabreLite嵌入式设备上实例化并评估了PARseL。