华为TEE通过CC EAL5+认证 采用形式化方法设计
陈拾九移动支付网2019/9/30 9:31:33

9月26日下午,华为2019年度旗舰新品发布会在上海举行,Mate30系列正式亮相国内。在Mate 30系列具有的多种功能、特性之中,其安全水平吸引了安全界人士的注意。Mate 30系列搭配了EMUI10,生物信息和密码储存在硬件隔离的TEE之中,并在TEE内完成运算,从而保障敏感信息的安全。

使用TEE保护敏感信息安全已经不是新鲜事情,华为P9就具有这一能力。Mate 30系列之所以引起安全界人士关注,是因为其TEE通过了CC EAL5+认证。通过CC EAL5+认证,意味着华为TEE具有了真正的硬件级安全。

微内核发力半形式化设计

TEE是基于硬件隔离的可信执行环境,和RichOS(Android、iOS)一起运行,功能为隔离Rich OS及其应用程序对硬件和软件安全资源的访问,从而保证安全。但是由于TEE技术本身的局限性,其安全性能认证一般只能达到CC EAL2+,TEE+SE方案能通过CC EAL5+认证。CC EAL5+甚至于6+一般属于安全芯片性能认证。

会有这样的认识是因为在Mate 30系列之前,只有芯片可以通过CC EAL5+及以上认证,且不是所有公司都可以通过该项认证,国内众多芯片公司也是近几年才开发出相关产品,陆续通过CC EAL5+认证。那么华为是怎么将软件做到硬件级别安全的呢?

据移动支付网了解,本次华为通过CC EAL5+的检测的系统为鸿蒙V1.2。该系统使用了微内核技术,通过形式化方法(Formal Method)完成了TEE设计。所谓形式化方法,是使用数学方法解决软件问题,主要包括建立精确的数学模型以及对模型的分析活动,具体可以理解为是运用形式化语言,进行形式化的规格描述、模型推理和验证的方法。

TUV证书报告截图

形式化方法开发出来的软件系统可通过数据模型验证所有软件运行路径,这是之前方法学设计无法做到的,如果说方法学设计对于安全防护是见招拆招,那么形式化方法设计可以在见招拆招的基础上进行预见性防御。

但是形式化方法由于其使用大量数学理论,将限制大多数程序设计人员的学习和使用;对于较小规模的项目形式化方法是有效的,但却很难应用于一些大型系统;也会造成项目开发周期变长,项目费用增高等问题,是一项具有争议的技术。但是使用形式化方法进行开发、测试是通过EAL5的必须要素。

微内核技术是指将操作系统中更多的成分和功能放到更高的层次(即用户模式)中去运行,留下一个尽量小的内核完成操作系统最基本的核心功能。据移动支付网了解,目前TEE使用微内核技术的有华为、豆荚、高通和Trustonic四家公司。

华为使用微内核技术重新构架了TEE内的操作系统,TEE相关从业人士形容为“系统内再写了一个系统”。

专家表示,想要完成这样的设计,需要和硬件有极高的契合度,华为自研的麒麟990无疑是符合这个要求的。总的来说,华为TEE通过CC EAL5+认证是麒麟990芯片、形式化方法和微内核技术的共同作用结果。

有必要通过EAL5+吗?

在华为发布的上一代旗舰P30系列手机中使用了TEE+inSE安全方案,其中inSE方案通过了EMVCo认证,具有金融级硬件安全等级。也就是说,现有的TEE+inSE安全方案可以满足现有的安全需求。

升级TEE通过CC EAL5+绝对不是什么轻松的事情,2016年同方微电子突破CC EAL5+认证时,时任同方微电子总裁段立用一句话总结了全过程:“过程惨不忍睹,结果超乎预料”,可见过程之艰辛。在目前安全方案完全可以满足行业需求的情况下,华为有必要通过这个CC EAL5+认证吗?

业内人士表示,此举可能是为了布局未来5G物联网时代。在未来5G物联网时代,可以预见绝大部分电子产品将带有联网互动功能以满足多种需求,在这种情况下,个人信息安全、生物信息安全将会受到严峻考验。TEE是目前各种安全方案中兼顾安全和便捷性的,可以方便的部署于物联网产品中。业内人士表示,高安全性能的TEE或将得到市场青睐。

目前国内TEE产品最高通过CC EAL2+认证,华为此举会不会引起业界的“军备竞赛”,业内人士表示,华为TEE方案肯定会引起业内企业的追逐,但由于华为TEE和其麒麟芯片990关系密切,其他企业可能会面临技术难题。

本文为作者授权发布,不代表移动支付网立场,转载请注明作者及来源,未按照规范转载者,移动支付网保留追究相应责任的权利。

展开全文
相关阅读
资讯查询取消