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

Border Patrol: Improving Smart Device Security through Type-Aware Systems Design

边境巡逻：通过类型感知系统设计提高智能设备安全性

基本信息

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

来源：
https://gtr.ukri.org/projects?ref=EP%2FN028201%2F1
关键词：
Border Patrol Improving Smart Device

项目摘要

There are increasing concerns about the safety and security of critical infrastructure such as nuclear power plants, the electricity grid and other utilities in the face of possible cyber attacks. As ageing controllers are replaced by smart devices based on Field-Programmable Gate Arrays (FPGAs) and embedded microprocessors, the safety of such devices raises many concerns. In particular, there is the very real risk of malicious functionality hidden in the silicon or in software binaries, dormant and waiting to be activated. Currenthardware and software systems are of such complexity that it is impossible to discover such malicious code through testing. We aim to address this problem by closely connecting the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system will be used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification. Static type checking of data types and multiparty session types can ensure the correctness of the interaction between the components. However, as static checking assume full access to the design source code it cannot be used to protect against potential threads issuing from third-party functional blocks (know as ``Intellectual Property Cores'' or IP cores) that are commonly used in hardware design:the provider of the IP core can claim adherence to the types and protocols, so that the IP core will meet the compile-time requirements, but the run-time the behaviour cannot be controlled using static techniques. The same applies to third-party compiled software libraries.Therefore we propose to use run-time checking of data types as well as session types at the boundaries of untrusted modules ("Border Patrol"), so that any intentional or unintentionalbreach of the specification will safely be intercepted.

面对可能的网络攻击，人们越来越担心核电站、电网和其他公用事业等关键基础设施的安全和安保。随着老化的控制器被基于现场可编程门阵列（FPGA）和嵌入式微处理器的智能设备所取代，这些设备的安全性引起了许多关注。特别是，存在非常真实的风险，恶意功能隐藏在芯片或软件二进制文件中，处于休眠状态并等待被激活。目前的硬件和软件系统是如此的复杂，以至于不可能通过测试发现这种恶意代码。我们的目标是解决这个问题，通过使用一个正式的设计方法，基于静态和动态类型检查的类型系统的实际执行紧密连接的系统设计规范。类型系统将被用作一种形式语言来对设计规范进行编码，以便根据规范自动检查实际实现。数据类型和多方会话类型的静态类型检查可以确保组件之间交互的正确性。然而，由于静态检查假设对设计源代码的完全访问，因此它不能用于防止来自硬件设计中常用的第三方功能块（称为“知识产权核心”或IP核心）的潜在线程：IP核心的提供商可以声称遵守类型和协议，因此IP核心将满足编译时要求，但运行时行为不能使用静态技术进行控制。这同样适用于第三方编译的软件库。因此，我们建议在不受信任的模块（“边界巡逻”）的边界上使用数据类型和会话类型的运行时检查，以便安全地拦截任何有意或无意的违反规范的行为。