权益分类	功能权益	普通用户	{{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/N028201/1）的主题，该项目将持续到2023年，因此与当前提案具有巨大的协同潜力。在我们当前的EPSRC项目Border Patrol （EP/N028201/1）中，我们通过设计基于硬件ip核的soc来研究数字安全。关键的机制是使用类型驱动的按规范设计。设计的规范在类型系统中编码，因此实现必须遵循规范。对于受信任的模块，可以在设计时强制遵守规范；对于不受信任的模块，可以在运行时强制遵守规范，方法是使用基于fsm的运行时类型检查器巡视不受信任模块的边界。