服務國家航天航空等重大工程，

為國產軌道交通

提供安全可信保障技術，

助力上海地鐵線實現無人駕駛，

……

在上海有這樣一個實驗室

為我國航空航天、軌道交通、

電力控制等安全攸關領域，

提供了自主可控、高度可信的

中樞神經。

上海市高可信計算重點實驗室

始建于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 年國家科技進步二等獎。

繼往開來，砥礪前行，

實驗室將繼續圍繞

可信軟件領域的關鍵技術

進行攻關，

著力突破“卡脖子”難題，

努力培養和造就一支

具有全球視野的科學家群體，

并建設成為

在軟件工程領域具有重大影響力、

引領相關學科發展

并具有強大凝聚力的研究基地，

為上海科創中心建設提供持續支持、

為建設科技強國貢獻一份力量。