服务国家重大科技发展战略，攻克可信软件卡脖子难题上海市高可信计算重点实验室

　　服务国家航天航空等重大工程，
　　为国产轨道交通
　　提供安全可信保障技术，
　　助力上海地铁线首次实现无人驾驶，
　　……
　　在上海有这样一个实验室
　　为我国航空航天、轨道交通、
　　电力控制等安全攸关领域，
　　提供了自主可控、高度可信的
　　中枢神经。
　　上海市高可信计算重点实验室
　　始建于2007年12月，
　　2009年7月
　　经上海市科委批准正式运行，
　　创建者为
　　中国科学院院士何积丰教授。
　　20世纪80年代，何积丰院士被学校先后派往美国斯坦福大学、英国牛津大学进修学习。在牛津大学进修期间，他与英国计算机科学家、图灵奖获得者托尼·霍尔一起创造性地提出了软件领域的程序统一理论（UTP），并由此开创了程序统一理论的国际学派。
　　2001年，他响应党和国家号召，受命组建国家首批示范性软件学院之一的华东师范大学软件学院。何积丰院士关注国家与社会的发展需求，并积极有效地推动产学研融合。
　　自2007年起，他担任国家自然科学基金委＂可信软件基础研究＂重大研究计划的首席科学家，并创建了＂上海市高可信计算重点实验室＂，为可信软件技术在国内的普及与应用作出了杰出贡献。
　　实验室依托华东师范大学，以当前计算机科学和软件工程领域提出的可信计算和安全软件的基本问题为背景，面向国家发展软件产业的战略需求和上海市地方经济的重点需求，确立了高可信计算理论、可信软件构造平台和可信计算应用等为主攻方向，进行可信计算理论与软件开发技术的基础研究。
　　十余年来，实验室服务于
　　国家重大科技发展战略，
　　已形成了一系列具有影响力的成果。
　　对接国家关键领域重大需求，
　　攻克可信软件＂卡脖子＂难题
　　实验室主任邓玉欣教授向记者介绍，
　　围绕软件＂安全可靠、自主可控＂国家战略，
　　实验室团队潜心攻坚
　　工业控制软件可信保障＂卡脖子＂难题，
　　联合航空航天、汽车电子等
　　行业龙头企业，
　　承担国家重大研究任务，
　　开展工控领域可信技术研发，
　　形成国际领先前沿技术成果，
　　打破国外技术封锁与垄断，
　　显著提升我国
　　可信工控软件整体研发水平，
　　成果获 2019 年度
　　上海市科技进步特等奖。
　　实验室
　　攻克工业控制软件安全可信理论难题，
　　服务国家航天航空等重大工程。
　　针对我国重大工业装备控制软件开发技术与工具长期受制于国外的困局，实验室聚焦软件正确性与安全性核心问题，提出并发程序的统一模型框架，形成系统化的工业控制软件安全可信保障方法，突破软件自动化分析、验证及测试等关键技术，自主研发覆盖软件全生命周期的开发与验证工具链，实现工业控制软件开发环境的自主可控。成果应用于国产大型客机发动机研制、探月工程等重大任务。
　　据介绍，
　　实验室联合龙头企业
　　成立院士工作站，
　　为国产轨道交通
　　提供安全可信保障技术。
　　研发列车信号控制系统的建模与验证工具链，应用于卡斯柯信号有限公司国产轨道交通信号控制系统，使其千行代码缺陷率降低 50%，测试成本降低 40%，开发周期缩短 15%。验证后的系统通过国际最高安全等级莱茵 SIL4 级认证。该系统服务于上海首条 GoA 三级地铁线路等国内近 30 条线路以及埃及斋月十日城等 4 条国外线路，成功实现国产信号控制系统＂走出去＂战略目标。
　　此外，实验室联合普华基础软件、中电科集团、上汽集团等著名企业，承担国家汽车电子操作系统核高基项目，首次将形式化验证方法应用于汽车电子操作系统的研发，所研发的实时操作系统代码可信保障技术推动了汽车电子操作系统内核 ORIENTAIS 通过国际 OSEK 标准认证。该系统已在包括上汽荣威等国产品牌汽车上装载，并成功打入欧洲市场。
　　突破信息安全技术瓶颈，
　　创构国家新型基础设施安全防护
　　邓玉欣教授介绍，
　　实验室围绕国家新型基础设施
　　安全重大战略需求，
　　建立安全保障理论体系，
　　突破安全防护技术瓶颈，
　　提升重点行业攻防渗透能力，
　　助力重点行业及国家党政军系统防护。
　　破解云计算安全难题，构建安全保障理论体系。实验室首次构建各类函数在密文域上可批量验证计算正确性的安全外包计算理论，解决传统公钥全同态加密计算与通信开销巨大的问题；基于可追踪、可撤销属性基代理重加密，解决云存储数据的轻量化完整性安全审计和灵活受控转移问题。获 2018 年教育部自然科学一等奖。
　　突破高级可持续性威胁攻击安全防护技术，服务国家重大工程。实验室研发恶意代码特征提取、变种检测及未知协议解析机制，提出 APT 攻击行为检测方法和可疑攻击溯源机制。服务党政系统安全检测及国家电网安全免疫工程。成果获 2017 年度教育部技术发明一等奖。
　　聚焦网联汽车安全需求，提升汽车信息安全攻防渗透能力。实验室按照 ISO21443 和美国 SAE 标准搭建汽车信息安全仿真验证平台，突破自动驾驶安全入侵检测防御技术，建立自动驾驶安全策略库，研发首款车载 T-box、车机 IVI 等信息安全合规性检测工具，已服务于上汽集团、广汽集团提升智能网联汽车信息安全防护体系建设。
　　实践＂自主可控、安全可靠＂战略，
　　自主研发新一代分布式数据库系统
　　数据库系统是
　　现代信息社会的重要基础设施，
　　支撑了现实世界中的
　　关键核心业务。
　　为了应对国家对技术自主可控的需求以及传统行业互联网化、新兴互联网经济快速发展带来的技术挑战，数据库团队研发了支持关键业务的新一代分布式数据库系统，并将其应用在多个国家重点行业的核心业务系统中，促进自主研发数据库在这些关键领域的应用。
　　据了解，
　　实验室提出了解决电信和金融等行业
　　关键核心业务处理中
　　＂现象级＂应用的
　　高并发负载难题的方案，
　　突破了互联网上的系统难以兼顾
　　高可用与数据一致性的困境，
　　可满足7*24高可用要求，
　　并支持关键核心业务互联网化
　　对复杂查询的性能要求。
　　自主研发出可扩展数据库管理系统，
　　率先在五大国有银行之一的交通银行
　　实现其核心数据库建设与应用改造，
　　已安全运行 100 多个业务应用，
　　助力企业降本增效并取得显著经济效益。
　　相关成果获
　　2019 年国家科技进步二等奖。
　　继往开来，砥砺前行，
　　实验室将继续围绕
　　可信软件领域的关键技术
　　进行攻关，
　　着力突破＂卡脖子＂难题，
　　努力培养和造就一支
　　具有全球视野的科学家群体，
　　并建设成为
　　在软件工程领域具有重大影响力、
　　引领相关学科发展
　　并具有强大凝聚力的研究基地，
　　为上海科创中心建设提供持续支持、
　　为建设科技强国贡献一份力量。