Safety and security issues in programmable IoT systems are still a pressing problem. Many solutions have been proposed to curb unexpected behavior of automation apps installed on IoT platforms by enforcing safety and security policies at runtime. However, all prior work addresses a weaker version of the actual problem as they consider a simple threat model, which is far from the reality. Moreover, these solutions are heavily dependent on the installed apps and catered to specific IoT platforms, which can unfortunately result in inaccurate runtime enforcement of policies. In this paper, we address a stronger version of the problem by considering a realistic threat model, where (i) undesired cyber actions (e.g., lock()/unlock()) can come from not only automation platform backends (e.g., SmartThings) but also close-sourced thirdparty services (e.g., IFTTT), and (ii) physical actions (e.g., user interactions) on devices can move the IoT system to an unsafe state. We propose a runtime mechanism, dubbed Maverick, which employs an app-independent, platform-agnostic mediator to enforce policies against all undesired cyber actions and applies corrective-actions to bring the IoT system back to a safe state if it ever transitions to an unsafe state. To assist users for writing policies, Maverick is equipped with a policy language capable of expressing rich temporal invariants and an automated toolchain that includes a policy synthesizer and a policy analyzer. We implemented Maverick in a prototype and showed its efficacy in both physical and virtual testbeds where it incurred minimal overhead.

翻译：可编程物联网系统的安全与安保问题仍是亟待解决的难题。已有诸多方案通过运行时强制执行安全及安保策略来抑制物联网平台上自动化应用（apps）的意外行为。然而，所有先前工作仅考虑了与现实相距甚远的简单威胁模型，仅触及实际问题的弱化版本。此外，这些方案严重依赖已安装的应用且专为特定物联网平台设计，这可能导致策略的运行时强制执行不准确。本文通过考虑更贴合实际的威胁模型来应对问题的强化版本：在此模型中，(i) 不期望的网络行为（如lock()/unlock()）不仅可能来自自动化平台后端（如SmartThings），还可能源于闭源第三方服务（如IFTTT）；(ii) 设备上的物理行为（如用户交互）可能将物联网系统推向不安全状态。我们提出一种运行时机制——Maverick，该机制采用应用无关、平台无感的调解器（mediator）对所有不期望的网络行为强制执行策略，并在系统可能进入不安全状态时施加纠正操作（corrective-actions）使其恢复至安全状态。为助力用户编写策略，Maverick配备了一种能够表达丰富时序不变量的策略语言，以及包含策略综合器与策略分析器的自动化工具链。我们在原型系统中实现了Maverick，并在物理与虚拟测试床上验证了其有效性，实验表明该机制引入了极低的运行时开销。