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