射频优卡多芯片操作系统隔离与安全通信方法研究

摘要

智能卡作为个人数据载体已广泛应用于生产生活中的各个领域。随着应用的普及，智能卡发行数量剧增，导致单个用户卡携带不便和卡资源管理的复杂。同时，智能卡的多次重复发行，且用户手中大部分智能卡大部分时间处于非工作状态，导致卡软硬件资源的重复配置与闲置浪费。由于现行多应用智能卡只支持单个芯片操作系统（Chip Operating System，简称COS），不同COS所支持的卡应用程序间存在不兼容性，故多应用智能卡未能有效解决传统智能卡的便携性和资源闲置浪费问题。
　　 射频优卡的出现为上述问题的解决提供一个很好的技术思路。射频优卡在体系结构上集成相互独立的现行多个COS及应用；在通信接口上采用射频实现非接触通信。
　　 这些特点使得射频优卡在有效解决日益严峻的多卡携带问题，优化卡资源利用的同时，提供卡应用的快速自动处理。但同时，射频优卡的多操作系统架构及无线信道通信，引发了两大关键安全问题：卡内的多COS 安全隔离与卡外的射频通信安全。
　　 基于射频优卡体系结构特点，分析其生命周期中涉及的各种安全角色，建立多级安全依赖关系。根据每次用卡中的状态转移路径，建立运行时k-COS和k-block（存储块）的有限状态机模型。采用计算树逻辑语言对运行时安全属性进行形式化定义；
　　 使用基于有序二元决策图的符号模型验证规范语言对有限状态机模型进行系统说明；运行符号模型验证器检验安全模型对于安全属性的满足性。验证结果表明，多COS 射频优卡运行时有限状态机模型满足运行时三大安全属性，并表明符号模型验证对于COS数量小于10的射频优卡运行时安全模型是一种可行的形式化验证方法。
　　 基于可编程动态地址总线的隔离机制通过对主CPU部分地址总线进行控制来限制运行COS的存储访问。由于地址映射控制参数可能遭受非法篡改，该机制可能出现运行时的非法数据访问。从现实生活中会议的组织模式得到启发，提出一种基于席位约束会议模型的隔离机制，该机制在射频优卡的硬件层增加一个类似于会议中主席台的专用主席台存储器来存储运行COS所需的代码与数据。与可编程动态地址总线隔离机制不同，会议模型隔离机制不需对主CPU的地址总线做任何限制，而由主席台存储器提供一个隔离域来限制运行COS的存储访问。由于主席台存储器的易失性，且与其它存储器在物理上是隔离的，从而保证运行COS与其它COS的完全隔离。功能仿真表明，会议模型隔离机制能够提供很好的运行时安全隔离环境。
　　 射频优卡系统由于射频信道的开放性，在链路层上存在多卡冲突问题。基于对单读写器系统卡输入过程、服务时间分布和服务规则的分析，建立多卡识别过程的排队模型，对系统达到统计平衡状态下读写器识别范围内卡的概率分布、平均卡数及卡的平均逗留时间进行数学分析。借鉴已有算法中的帧长及卡应答概率调整策略，设计一种双边同步动态调整SDA（Synchronous Dynamic Adjusting）算法。SDA 根据上一轮阅读循环的冲突状况，在读写器和射频优卡双边分别调整帧长和应答概率。
　　 软件仿真表明，当服务卡数大于100时，若卡平均到达率在0.5与2之间变化，卡初始应答概率为0.875 或1.0时，SDA算法将达到最优识别率。在相同的仿真条件下，SDA总的服务时间、卡的平均逗留时间和识别率均优于两种典型的射频识别系统多标签冲突解决算法。
　　 射频优卡系统由于信道的开放性和非对称性，在实际应用环境中会受到各种可能的攻击。基于对攻击的分析，提出射频优卡系统应用层的安全需求；基于读写器角色分配与授权，设计一种双向认证保护协议。协议采用动态身份更新机制防止重发攻击和位置跟踪；采用单向哈希函数防止数据侦听和向前递推分析攻击；采用会话密钥备份机制防止数据异步攻击；采用读写器访问权限检测防止合法读写器的非授权数据访问。性能分析表明，所设计的协议是一种安全、高效、低成本、易实现的安全认证协议。