权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

AppControl: Enforcing Application Behaviour through Type-Based Constraints

AppControl：通过基于类型的约束强制应用程序行为

基本信息

批准号：
EP/V000462/1
负责人：
Wim Vanderbauwhede
金额：
$ 188.97万
依托单位：
University of Glasgow
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2020
资助国家：
英国
起止时间：
2020 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FV000462%2F1
关键词：
AppControl Enforcing Application Behaviour through

项目摘要

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.

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