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

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

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.