在支持WiFi、蓝牙、ZigBee、LoRa等异构协议通信的基础上，基于身份认证、数据加密、数据脱敏、流量整形等防御策略，实现物联网下的用户隐私保护，数据保密传输。

云边协同：在云侧实现对网关应用的全生命周期管理（创建、配置、卸载、更新、监控和日志采集），完成对网关配置，边缘侧使用K8s进行任务调度管理，以及计算模型训练，并下发给网关更新和执行。

安全的设备识别：设备处于物联网最底层，也是物联网中存在最为广泛的节点，设备的严格准入控制，是物联网安全的第一道防线。物联网要求能够对接入的设备进行智能的识别，以期在最底层实现设备安全识别，识别有风险的物联网设备，阻止虚假设备入网。

安全的身份认证：身份认证为物联网设备节点提供通行凭证。该物联网网关旨在以物联网设备标识，结合国密SM9算法实现安全身份认证，并为上层功能或服务提供设备标识，或身份凭证，实现设备可信。

安全的访问控制：访问控制是为网关提供的计算或数据资源以准入控制。为实现多源异构网络的安全访问控制，在域内要实现基于标识的访问控制，在域间实现基于区块链的多级访问控制。

安全的数据传输：攻击者可能会对数据传输的流量特征进行分析，从而获得系统数据的某些特征，为在数据传输的过程中对数据进行保护，网关引入流量伪装技术。

   安全的数据隐私：数据隐私的泄露可能会带来巨大的损失，因此网关拟采取数据加密传输，差分隐私，数据挖掘的隐私保护等技术对数据的隐私进行保护。

图1 安全网关样机

安全协议验证：协议的安全性检测是网络协议安全保护的重要环节。研究人员在设计或优化安全协议后，需要进一步证明该协议的安全。与非形式化的安全协议验证技术相比，形式化方法能够更全面、深入的检测安全协议和软件中未知的漏洞，它不仅能够证明安全协议的安全性，而且有助于发现针对安全协议的新型攻击手段。但是由于安全协议的复杂性，现有的形式化验证技术并不能自动化证明所有的安全协议和相关安全软件，在证明过程中需要专业验证人员辅助计算机完成证明。过高的人力成本和学习成本阻碍了形式化验证技术的进一步发展和运用。安全协议形式化自动验证技术的核心是将深度强化学习技术与形式化验证技术结合，使用动态策略对安全协议进行验证。主要流程如图2所示，包括两部分：形式化验证信息提取和协议验证。

图2 安全协议形式化自动验证技术

形式化验证信息提取：构建形式化证明与验证的底层框架，自动提取协议模型中的证明目标和证明过程中所用到的公理，从而构建定理树。由于协议的复杂性，无法一次性构建完整的定理树，因此将协议验证分为若干轮次，在每一轮根据强化学习神经网络选择的证明路径构建新的定理子树，并与之前轮次的定理树合并，以对定理树进行扩展。

协议验证：使用深度Q网络（DQN）评估定理树各节点成功完成验证的概率，根据评估结果自动生成证明路径。并判断证明路径的完整性和正确性。如果证明路径中存在循环，可能导致协议验证过程无法终止，给予该路径负反馈，并训练神经网络优化证明策略。如果证明路径不存在循环，但不完整，返回信息提取模块扩展定理树，以生成完整的证明路径。如果证明路径正确，即协议成功完成验证，系统自动终止，输出验证结果。

该方法突破并解决了传统形式化自动验证中的状态空间爆炸问题，并实现了对网络安全协议的自动化证明。研究成果可以挖掘给定目标的安全协议与软件的所有安全漏洞，确保网络安全协议不会被攻击者攻破。基于此研究成果，针对5G-AKA 协议的可追责属性进行了形式化分析，并发现协议设计存在缺陷。并实现了针对 PoW类共识协议、支付协议、矿池协议等区块链底层协议的更细粒度的形式化分析，发现了矿池协议中存在的一个新型安全漏洞。另外，实现了首个以太坊平台智能合约的全自动形式化验证工具。应火币网邀请，已对5个智能合约进行了形式化验证，发现并修复了所有安全漏洞。研究成果已经发表于USENIX Security 2020。以下视频为我们的网关原型系统的演示视频。

网关原型系统设计简介

检测非法摄像头接入