AppControl: Enforcing Application Behaviour through Type-Based Constraints

背景技术在当前技术水平下，可以限制在计算机系统上运行的第三方程序的访问权限。通过添加架构功能(如Cheri提供的功能)，可以实现前所未有的细粒度内存保护和隔离。然而，这些机制不足以控制程序的行为，使其遵循预期的规范。例如，如果程序执行网络访问，则不可能确保访问的网络位置是开发人员的预期结果，或者是系统中后门的结果。通常，这是由程序执行的任何系统调用的情况。因此，恶意程序可以参与DDoS攻击，或将有关系统的信息发送到命令和控制服务器等。库调用也是如此，它可以在进程的内存空间内执行未指定的操作。项目目的本项目的目标是通过功能硬件启用的设计规范增强关键任务片上系统设计的数字安全提供。这意味着片上系统有一个正式的、可执行的规范(通常由系统架构师创建)，SoC的每个软件组件都必须遵守该规范。规范不兼容的程序无法运行；未指定的运行时行为将引发异常。对于上面的例子，该规范可以管理网络访问，也可以管理对系统信息的访问。这一目标的实际实现是通过扩展编程语言来支持可表达的规范和工具链，以确保在运行时在功能硬件上强制执行规范。Nutshell我们对如何实现这一目标的愿景的关键思想是通过使用行为类型系统，即SoC及其每个单独组件的规范被表示为一个类型，它有效和正式地描述了每个组件允许的接口和交互。这种基于类型的规范将是程序可执行文件的一个组成部分，并由操作系统对照整个系统规范进行验证。该建议侧重于软件组件，并将建立在用于强制执行基于类型的规范的能力硬件上。基于类型的按规格设计硬件组件是EPSRC边境巡逻项目(EP/N028201/1)的主题，该项目将持续到2023年，因此具有与当前提案协同的巨大潜力。在我们当前的EPSRC项目边境巡逻(EP/N028201/1)工作之前，我们通过设计基于硬件IP核的SoC来研究数字安全。其关键机制是使用类型驱动的规范设计。设计的规范编码在类型系统中，因此实现必须遵循规范。对于受信任的模块，可以在设计时强制遵守规范，对于不受信任的模块，可以在运行时通过使用基于FSM的运行时类型检查器巡逻不受信任的模块的边界来强制遵守规范。

Background: The ProblemWith the current state of the art, it is possible to limit the access privileges of a third-party program running on a computer system. The addition of architectural capabilities such as provided by CHERI enable unprecedented fine-grained memory protection and isolation. These mechanisms are however not sufficient to control the behaviour of a program so that it follows the intended specification. For example, if a program performs network access, it is not possible to ensure that the network location accessed is intended by the developer, or the result of a backdoor in the system. In general, this is the case for any system call performed by the program. As a result, malicious programs can e.g. participate in DDoS attacks, or send information about the system to a Command and Control server, etc. It is also the case for library calls, which could perform unspecified actions within the memory space of a process.Project AimThe aim of this project is to enhance the provision of Digital Security By Design for mission-critical Systems-on-Chip through Capability hardware-enabled Design-by-Specification. What this means is that the Systems-on-Chip has a formal, executable specification (typically created by the system architect), and every software component of the SoC is forced to adhere to this specification. Programs with incompatible specifications cannot run; unspecified run-time behaviour will raise an exception. For the above example, the specification could govern the network access and also the access to system information. The practical realisation of this aim is through the extension of programming languages to supports expressive specifications and a toolchain which ensures that the specifications are enforced at run time on Capability hardware. Key Ideas in a NutshellOur vision of how to achieve this goal is through the use of behavioural type systems, i.e. the specification of the SoC and each of its individual components are expressed as a type, which effectively and formally describes the allowed interfaces and interactions of each component. This type-based specification will be an integral component of the program executable, and be validated against an overall system specification by the operating system.This proposal focuses on software components, and will build on the capability hardware for enforcement of the type-based specifications. The type-based Design-by-Specification of hardware components is the topic of the EPSRC Border Patrol project (EP/N028201/1), which will run until 2023 and therefore present great potential for synergies with the current proposal.Prior WorkIn our current EPSRC project Border Patrol (EP/N028201/1) we investigate digital security by design for the design of hardware IP-core based SoCs. The key mechanism is the use of type-driven design-by-specification. A design's specification is encoded in the type system, so that the implementation must follow the specification. Adherence to the spec can be enforced at design time for trusted modules, and at run time for untrusted modules by patrolling the untrusted module's borders with FSM-based run-time type checkers.