編者按
今天，移動互聯(lián)網無處不在，人工智能已經向我們走來，“用代碼改變世界”的流行語不再是程序員的自我調侃。現(xiàn)代信息社會對計算機系統(tǒng)的依賴，很大程度上體現(xiàn)為對軟件的依賴，計算機系統(tǒng)的缺陷很多情況下都由軟件問題引發(fā)。軟件系統(tǒng)能否在操作錯誤、環(huán)境影響、外部攻擊等干擾下，提供連續(xù)的服務，已成為一項嚴峻挑戰(zhàn)。
為此，計算機科學家提出了軟件“可信性”，這一在傳統(tǒng)的安全、可靠等概念基礎上發(fā)展起來的新概念。早在十多年前，中國科學家分析認為，軟件的運行環(huán)境和開發(fā)環(huán)境必將從傳統(tǒng)的封閉、靜態(tài)環(huán)境向開放、動態(tài)、多變的互聯(lián)網環(huán)境轉變，“可信軟件”將成為現(xiàn)代軟件技術發(fā)展和應用的重要趨勢和必然選擇。
2007年底，國家自然科學基金委員會啟動了“可信軟件基礎研究”重大研究計劃，投入經費1.9億元，至2016年底結題。
該重大研究計劃實施的十年間，研究人員以國家關鍵應用領域中軟件可信性問題為主攻目標，既有力推動了軟件基礎理論的探索與創(chuàng)新，又有效應對了軟件發(fā)展的重要科學挑戰(zhàn)，對促進我國軟件產業(yè)的振興與發(fā)展具有重大的現(xiàn)實意義。同時，還形成了一支以中青年人才為主力的高水平研究隊伍，培養(yǎng)了一批站在世界科學研究前沿的學科帶頭人。
本期基金版將總結該重大研究計劃取得的經驗，介紹面向航天嵌入式軟件、車聯(lián)網及網絡交易等三個行業(yè)的典型應用示范，充分展示該項目取得的成績。
看準趨勢
從“能不能”到“信不信”
2018年8月中旬，剛入秋的北京清晨已有些許涼意，中關村附近的一個菜市場內人群熙攘。挑選好幾樣蔬菜后，張大爺拿出兜里的智能手機，熟練地通過掃小攤上掛出的藍色二維碼支付了菜錢。和十多年前網上支付剛剛啟動時的情況不同，今天，即使上了年紀的大爺大媽們，也不會因為擔心手機支付不安全，而拒絕使用支付寶綁卡、掃碼支付。
人們對支付軟件的信任，來源于軟件本身的“可信性”，意指軟件系統(tǒng)是否能在操作錯誤、環(huán)境影響、外部攻擊等干擾下，依然提供連續(xù)的預期服務。
如今，以通信、存儲和計算為核心的信息基礎設施已經滲透人類生活的方方面面，軟件對“可信性”的要求，顯然不限于網絡支付領域。
早在十多年前，中國計算機學家已經注意到，隨著軟件的應用需求越來越多，復雜度越來越高，可用性要求越來越強，軟件系統(tǒng)也越來越龐大、越來越脆弱。“軟件不總是可以讓人信任的，很多時候它并不以人們所期望的方式工作，會發(fā)生各種故障和失效，從而直接或間接地對用戶造成巨大損害。”中科院院士、華東師范大學計算機科學與軟件工程學院教授何積豐表示。
1996年6月4日，歐洲阿麗亞娜5型火箭在首次發(fā)射中由于慣性參考系統(tǒng)軟件的數(shù)據(jù)轉換錯誤導致軟件失效，發(fā)射40秒后爆炸，造成25億美元的經濟損失。2005年11月1日，日本東京證券交易所由于軟件升級出現(xiàn)系統(tǒng)故障,導致股市停擺。2007年北京機場信息系統(tǒng)癱瘓，至少造成84個航班延誤。
在2017年12月舉行的國家自然科學基金委員會（以下簡稱基金委）可信軟件基礎研究重大研究計劃（以下簡稱重大研究計劃）結束評估會上，作為指導專家組組長的何積豐在報告中提及上述案例時，與會專家依然對過去種種因軟件可信性導致的損失感到萬分惋惜。
時間回溯到2007年底，面對當時由于網絡交互、共享、協(xié)同等帶來的“不可信”因素，基金委在廣泛聽取各界專家意見和反復深入研討的基礎上，由信息科學部、數(shù)學物理科學部和管理科學部聯(lián)合組織，及時啟動了該重大研究計劃。
用何積豐的話說，這是“我國軟件基礎研究領域的一件大事”。 “我們對軟件關注的重心從‘能不能’轉向了‘信不信’。”何積豐告訴《中國科學報》記者。
此后，國家層面相繼啟動了“863”計劃、“十二五”規(guī)劃等，支持相關領域的研究和發(fā)展。在業(yè)內專家看來，正是該重大研究計劃的啟動及基礎研究成果引領了國內這一領域的發(fā)展。
需求導向
直指“卡脖子”問題
圍繞可信軟件面臨的機遇和挑戰(zhàn)，科學家們將主攻問題鎖定在國家關鍵應用領域，并按“以重點領域應用需求為導向引領理論和技術研究、以理論和技術研究成果支撐綜合試驗平臺的研制、以綜合試驗平臺承載典型應用示范”的路線實施該重大研究計劃。
2010年至2013年，科學家們在陸續(xù)完成可信軟件理論體系和技術體系的積累后，將研究成果在各類試驗環(huán)境中進行示范，真正讓可信軟件技術走出實驗室，走進國民經濟主戰(zhàn)場。
本文開篇的場景中，人們對網絡支付的信任，得益于該重大研究計劃中建立的我國首個互聯(lián)網交易風險防控體系。這一體系已服務21個國家和地區(qū)的4億多支付寶實名用戶。該重大研究計劃科學家、同濟大學計算機系教授蔣昌俊介紹，該研究從運用到實踐3年來為支付寶減少資產損失173.03億元，資金損失率僅為十萬分之零點九，是發(fā)達國家同領域資金損失率的兩百分之一。
此外，還有1000多萬行代碼應用在我國探月工程、載人航天、北斗導航等型號的各類航天嵌入式軟件中，打破國外技術壟斷的列車通信控制器，3年為支付寶減少170余億元損失的首個互聯(lián)網交易風險防控體系，連續(xù)4年沒有發(fā)生重大事故的電子稅務可信監(jiān)控，實車接入超過7萬輛、世界上規(guī)模最大的實車實時數(shù)據(jù)處理平臺系統(tǒng)……據(jù)統(tǒng)計，該重大研究計劃在重大示范應用方面共完成項目15項，與長城華冠、中航工業(yè)615所、航天五院、全路通、核九院、支付寶等機構開展合作，推動國家安全相關行業(yè)自主可控技術發(fā)展。
談到收獲與感想，該重大研究計劃科學家、中國空間技術研究院楊孟飛院士表示：“重大研究計劃的實施過程中，我們邊研究、邊驗證、邊應用，軟件質量顯著提高、研制效率顯著提升，逐步實現(xiàn)了從局部到系統(tǒng)、從依賴人到依賴工具的轉變。”楊孟飛院士介紹，“集成項目實施以來，軟件交付的缺陷率顯著下降，百余個航天器在軌運行未發(fā)生軟件質量問題。”
在科學家們看來，以需求為導向開展基礎研究，切實解決了諸多領域中的“卡脖子”問題，有力支撐了國家戰(zhàn)略。
完善體系
引領該領域由弱到強
在重大應用示范取得成功的背后，離不開基礎理論研究和技術創(chuàng)新平臺的突破。該重大研究計劃啟動之初，指導專家便對長達十年的科學研究繪制了藍圖，不僅提出了科學目標、研究內容要點和核心科學問題，還精心對目標進行分解，制訂了進度計劃。
十年里，科學家們圍繞“軟件可信性度量與建模”“可信軟件的構造與驗證”“可信軟件的演化與控制”和“可信環(huán)境的構造與評估”等四個核心科學問題取得了豐碩成果。
“共發(fā)表2641篇論文，其中SCI檢索803篇，EI檢索1495篇；國家級科技獎勵共計12項，省部級獎勵31項。”何積豐用數(shù)據(jù)勾勒出該重大研究計劃取得成果的概況。
這些數(shù)據(jù)反映的是，我國可信軟件基礎理論研究實現(xiàn)了跨越式發(fā)展。例如，可信軟件理論與方法元級框架的提出，實現(xiàn)了從傳統(tǒng)正確性向開放、動態(tài)、多變環(huán)境下的軟件可信性跨越；標準化科學化的可信計算環(huán)境構造與評估體系的建立，實現(xiàn)了從部分環(huán)節(jié)可信計算向全棧化可信計算跨越；軟件過程和制品的可信性度量體系的建立，實現(xiàn)了從分散的可信側面度量向系統(tǒng)化度量跨越；網絡軟件監(jiān)控與演化的一體化設計體系的提出，實現(xiàn)了從靜態(tài)補丁式演化向動態(tài)模型驅動體系結構的跨越。
同時，基礎研究的跨越發(fā)展牽引帶動了技術平臺實現(xiàn)創(chuàng)新性突破，多項關鍵技術集成，為軟件全生命周期工具集的設計奠定了技術基礎。例如，提出了基于基準測試的代碼級可信保障工具評價方法，研制了一批自主軟件工具，建立了基于虛擬機架構的可信云計算支撐環(huán)境。
2016年，英國皇家工程院院士、英國倫敦大學教授彼得·奧赫閱讀中國學者在計算機領域頂級會議“計算機輔助驗證”（CAV）發(fā)表的論文后，高度評價稱“這正是我所渴望的工作”。
十年來，一支以中青年人才為主力的高水平研究隊伍、一批站在世界科學研究前沿的學科帶頭人，也在該重大研究計劃實施過程中成長起來。來自我國70多家單位的1000多名計算機領域的學者合力攻關，共同推動我國可信軟件實現(xiàn)從小到大、從散到整、由弱到強的跨越式發(fā)展，進入該研究領域國際先進行列。
面向未來，何積豐表示：“為鞏固和輻射本重大研究計劃的成果，應及時建設可信軟件開發(fā)資源共享與服務平臺，充分利用群體智慧，建立形成可信軟件的開放數(shù)據(jù)、開放服務、讓合作開發(fā)成為可能。”
同時，科學家們也期待，在可信軟件與人工智能交叉的新領域有所作為，以滿足我國工業(yè)4.0和機器人等國家創(chuàng)新計劃對可信智能化軟件不斷增長的迫切需求。
摘自《中國科學報》
