編者按

今天，移動(dòng)互聯(lián)網(wǎng)無(wú)處不在，人工智能已經(jīng)向我們走來(lái)，“用代碼改變世界”的流行語(yǔ)不再是程序員的自我調侃?，F代信息社會(huì )對計算機系統的依賴(lài)，很大程度上體現為對軟件的依賴(lài)，計算機系統的缺陷很多情況下都由軟件問(wèn)題引發(fā)。軟件系統能否在操作錯誤、環(huán)境影響、外部攻擊等干擾下，提供連續的服務(wù)，已成為一項嚴峻挑戰。

為此，計算機科學(xué)家提出了軟件“可信性”，這一在傳統的安全、可靠等概念基礎上發(fā)展起來(lái)的新概念。早在十多年前，中國科學(xué)家分析認為，軟件的運行環(huán)境和開(kāi)發(fā)環(huán)境必將從傳統的封閉、靜態(tài)環(huán)境向開(kāi)放、動(dòng)態(tài)、多變的互聯(lián)網(wǎng)環(huán)境轉變，“可信軟件”將成為現代軟件技術(shù)發(fā)展和應用的重要趨勢和必然選擇。

2007年底，國家自然科學(xué)基金委員會(huì )啟動(dòng)了“可信軟件基礎研究”重大研究計劃，投入經(jīng)費1.9億元，至2016年底結題。

該重大研究計劃實(shí)施的十年間，研究人員以國家關(guān)鍵應用領(lǐng)域中軟件可信性問(wèn)題為主攻目標，既有力推動(dòng)了軟件基礎理論的探索與創(chuàng )新，又有效應對了軟件發(fā)展的重要科學(xué)挑戰，對促進(jìn)我國軟件產(chǎn)業(yè)的振興與發(fā)展具有重大的現實(shí)意義。同時(shí)，還形成了一支以中青年人才為主力的高水平研究隊伍，培養了一批站在世界科學(xué)研究前沿的學(xué)科帶頭人。

本期基金版將總結該重大研究計劃取得的經(jīng)驗，介紹面向航天嵌入式軟件、車(chē)聯(lián)網(wǎng)及網(wǎng)絡(luò )交易等三個(gè)行業(yè)的典型應用示范，充分展示該項目取得的成績(jì)。

看準趨勢

從“能不能”到“信不信”

2018年8月中旬，剛入秋的北京清晨已有些許涼意，中關(guān)村附近的一個(gè)菜市場(chǎng)內人群熙攘。挑選好幾樣蔬菜后，張大爺拿出兜里的智能手機，熟練地通過(guò)掃小攤上掛出的藍色二維碼支付了菜錢(qián)。和十多年前網(wǎng)上支付剛剛啟動(dòng)時(shí)的情況不同，今天，即使上了年紀的大爺大媽們，也不會(huì )因為擔心手機支付不安全，而拒絕使用支付寶綁卡、掃碼支付。

人們對支付軟件的信任，來(lái)源于軟件本身的“可信性”，意指軟件系統是否能在操作錯誤、環(huán)境影響、外部攻擊等干擾下，依然提供連續的預期服務(wù)。

如今，以通信、存儲和計算為核心的信息基礎設施已經(jīng)滲透人類(lèi)生活的方方面面，軟件對“可信性”的要求，顯然不限于網(wǎng)絡(luò )支付領(lǐng)域。

早在十多年前，中國計算機學(xué)家已經(jīng)注意到，隨著(zhù)軟件的應用需求越來(lái)越多，復雜度越來(lái)越高，可用性要求越來(lái)越強，軟件系統也越來(lái)越龐大、越來(lái)越脆弱?！败浖豢偸强梢宰屓诵湃蔚?，很多時(shí)候它并不以人們所期望的方式工作，會(huì )發(fā)生各種故障和失效，從而直接或間接地對用戶(hù)造成巨大損害?！敝锌圃涸菏?、華東師范大學(xué)計算機科學(xué)與軟件工程學(xué)院教授何積豐表示。

1996年6月4日，歐洲阿麗亞娜5型火箭在首次發(fā)射中由于慣性參考系統軟件的數據轉換錯誤導致軟件失效，發(fā)射40秒后爆炸，造成25億美元的經(jīng)濟損失。2005年11月1日，日本東京證券交易所由于軟件升級出現系統故障,導致股市停擺。2007年北京機場(chǎng)信息系統癱瘓，至少造成84個(gè)航班延誤。

在2017年12月舉行的國家自然科學(xué)基金委員會(huì )（以下簡(jiǎn)稱(chēng)基金委）可信軟件基礎研究重大研究計劃（以下簡(jiǎn)稱(chēng)重大研究計劃）結束評估會(huì )上，作為指導專(zhuān)家組組長(cháng)的何積豐在報告中提及上述案例時(shí)，與會(huì )專(zhuān)家依然對過(guò)去種種因軟件可信性導致的損失感到萬(wàn)分惋惜。

時(shí)間回溯到2007年底，面對當時(shí)由于網(wǎng)絡(luò )交互、共享、協(xié)同等帶來(lái)的“不可信”因素，基金委在廣泛聽(tīng)取各界專(zhuān)家意見(jiàn)和反復深入研討的基礎上，由信息科學(xué)部、數學(xué)物理科學(xué)部和管理科學(xué)部聯(lián)合組織，及時(shí)啟動(dòng)了該重大研究計劃。

用何積豐的話(huà)說(shuō)，這是“我國軟件基礎研究領(lǐng)域的一件大事”。 “我們對軟件關(guān)注的重心從‘能不能’轉向了‘信不信’?！焙畏e豐告訴《中國科學(xué)報》記者。

此后，國家層面相繼啟動(dòng)了“863”計劃、“十二五”規劃等，支持相關(guān)領(lǐng)域的研究和發(fā)展。在業(yè)內專(zhuān)家看來(lái)，正是該重大研究計劃的啟動(dòng)及基礎研究成果引領(lǐng)了國內這一領(lǐng)域的發(fā)展。

需求導向

直指“卡脖子”問(wèn)題

圍繞可信軟件面臨的機遇和挑戰，科學(xué)家們將主攻問(wèn)題鎖定在國家關(guān)鍵應用領(lǐng)域，并按“以重點(diǎn)領(lǐng)域應用需求為導向引領(lǐng)理論和技術(shù)研究、以理論和技術(shù)研究成果支撐綜合試驗平臺的研制、以綜合試驗平臺承載典型應用示范”的路線(xiàn)實(shí)施該重大研究計劃。

2010年至2013年，科學(xué)家們在陸續完成可信軟件理論體系和技術(shù)體系的積累后，將研究成果在各類(lèi)試驗環(huán)境中進(jìn)行示范，真正讓可信軟件技術(shù)走出實(shí)驗室，走進(jìn)國民經(jīng)濟主戰場(chǎng)。

本文開(kāi)篇的場(chǎng)景中，人們對網(wǎng)絡(luò )支付的信任，得益于該重大研究計劃中建立的我國首個(gè)互聯(lián)網(wǎng)交易風(fēng)險防控體系。這一體系已服務(wù)21個(gè)國家和地區的4億多支付寶實(shí)名用戶(hù)。該重大研究計劃科學(xué)家、同濟大學(xué)計算機系教授蔣昌俊介紹，該研究從運用到實(shí)踐3年來(lái)為支付寶減少資產(chǎn)損失173.03億元，資金損失率僅為十萬(wàn)分之零點(diǎn)九，是發(fā)達國家同領(lǐng)域資金損失率的兩百分之一。

此外，還有1000多萬(wàn)行代碼應用在我國探月工程、載人航天、北斗導航等型號的各類(lèi)航天嵌入式軟件中，打破國外技術(shù)壟斷的列車(chē)通信控制器，3年為支付寶減少170余億元損失的首個(gè)互聯(lián)網(wǎng)交易風(fēng)險防控體系，連續4年沒(méi)有發(fā)生重大事故的電子稅務(wù)可信監控，實(shí)車(chē)接入超過(guò)7萬(wàn)輛、世界上規模最大的實(shí)車(chē)實(shí)時(shí)數據處理平臺系統……據統計，該重大研究計劃在重大示范應用方面共完成項目15項，與長(cháng)城華冠、中航工業(yè)615所、航天五院、全路通、核九院、支付寶等機構開(kāi)展合作，推動(dòng)國家安全相關(guān)行業(yè)自主可控技術(shù)發(fā)展。

談到收獲與感想，該重大研究計劃科學(xué)家、中國空間技術(shù)研究院楊孟飛院士表示：“重大研究計劃的實(shí)施過(guò)程中，我們邊研究、邊驗證、邊應用，軟件質(zhì)量顯著(zhù)提高、研制效率顯著(zhù)提升，逐步實(shí)現了從局部到系統、從依賴(lài)人到依賴(lài)工具的轉變?！睏蠲巷w院士介紹，“集成項目實(shí)施以來(lái)，軟件交付的缺陷率顯著(zhù)下降，百余個(gè)航天器在軌運行未發(fā)生軟件質(zhì)量問(wèn)題?！?/p>

在科學(xué)家們看來(lái)，以需求為導向開(kāi)展基礎研究，切實(shí)解決了諸多領(lǐng)域中的“卡脖子”問(wèn)題，有力支撐了國家戰略。

完善體系

引領(lǐng)該領(lǐng)域由弱到強

在重大應用示范取得成功的背后，離不開(kāi)基礎理論研究和技術(shù)創(chuàng )新平臺的突破。該重大研究計劃啟動(dòng)之初，指導專(zhuān)家便對長(cháng)達十年的科學(xué)研究繪制了藍圖，不僅提出了科學(xué)目標、研究?jì)热菀c(diǎn)和核心科學(xué)問(wèn)題，還精心對目標進(jìn)行分解，制訂了進(jìn)度計劃。

十年里，科學(xué)家們圍繞“軟件可信性度量與建?！薄翱尚跑浖臉嬙炫c驗證”“可信軟件的演化與控制”和“可信環(huán)境的構造與評估”等四個(gè)核心科學(xué)問(wèn)題取得了豐碩成果。

“共發(fā)表2641篇論文，其中SCI檢索803篇，EI檢索1495篇；國家級科技獎勵共計12項，省部級獎勵31項?！焙畏e豐用數據勾勒出該重大研究計劃取得成果的概況。

這些數據反映的是，我國可信軟件基礎理論研究實(shí)現了跨越式發(fā)展。例如，可信軟件理論與方法元級框架的提出，實(shí)現了從傳統正確性向開(kāi)放、動(dòng)態(tài)、多變環(huán)境下的軟件可信性跨越；標準化科學(xué)化的可信計算環(huán)境構造與評估體系的建立，實(shí)現了從部分環(huán)節可信計算向全?；尚庞嬎憧缭?；軟件過(guò)程和制品的可信性度量體系的建立，實(shí)現了從分散的可信側面度量向系統化度量跨越；網(wǎng)絡(luò )軟件監控與演化的一體化設計體系的提出，實(shí)現了從靜態(tài)補丁式演化向動(dòng)態(tài)模型驅動(dòng)體系結構的跨越。

同時(shí)，基礎研究的跨越發(fā)展牽引帶動(dòng)了技術(shù)平臺實(shí)現創(chuàng )新性突破，多項關(guān)鍵技術(shù)集成，為軟件全生命周期工具集的設計奠定了技術(shù)基礎。例如，提出了基于基準測試的代碼級可信保障工具評價(jià)方法，研制了一批自主軟件工具，建立了基于虛擬機架構的可信云計算支撐環(huán)境。

2016年，英國皇家工程院院士、英國倫敦大學(xué)教授彼得·奧赫閱讀中國學(xué)者在計算機領(lǐng)域頂級會(huì )議“計算機輔助驗證”（CAV）發(fā)表的論文后，高度評價(jià)稱(chēng)“這正是我所渴望的工作”。

十年來(lái)，一支以中青年人才為主力的高水平研究隊伍、一批站在世界科學(xué)研究前沿的學(xué)科帶頭人，也在該重大研究計劃實(shí)施過(guò)程中成長(cháng)起來(lái)。來(lái)自我國70多家單位的1000多名計算機領(lǐng)域的學(xué)者合力攻關(guān)，共同推動(dòng)我國可信軟件實(shí)現從小到大、從散到整、由弱到強的跨越式發(fā)展，進(jìn)入該研究領(lǐng)域國際先進(jìn)行列。

面向未來(lái)，何積豐表示：“為鞏固和輻射本重大研究計劃的成果，應及時(shí)建設可信軟件開(kāi)發(fā)資源共享與服務(wù)平臺，充分利用群體智慧，建立形成可信軟件的開(kāi)放數據、開(kāi)放服務(wù)、讓合作開(kāi)發(fā)成為可能?！?/p>

同時(shí)，科學(xué)家們也期待，在可信軟件與人工智能交叉的新領(lǐng)域有所作為，以滿(mǎn)足我國工業(yè)4.0和機器人等國家創(chuàng )新計劃對可信智能化軟件不斷增長(cháng)的迫切需求。

摘自《中國科學(xué)報》