安全軟件理論與軟硬件協(xié)同設(shè)計(jì)可行性研究報(bào)告

安全軟件理論與軟硬件協(xié)同設(shè)計(jì)可行性研究報(bào)告一、項(xiàng)目定義1．項(xiàng)目名稱安全軟件理論與軟硬件協(xié)同設(shè)計(jì)2．項(xiàng)目領(lǐng)域本項(xiàng)目屬于基礎(chǔ)產(chǎn)業(yè)和高新技術(shù)領(lǐng)域，涉及計(jì)算機(jī)軟件與理論，系統(tǒng)芯片設(shè)計(jì)及計(jì)算機(jī)應(yīng)用等學(xué)科。二、項(xiàng)目背景1．項(xiàng)目背景軟件可靠性一直是計(jì)算機(jī)界關(guān)心的關(guān)鍵課題，1967年歐洲軟件工程先驅(qū)者Floyd提出用歸納斷言法來(lái)驗(yàn)證程序的正確性；1969年圖靈獎(jiǎng)獲得者Hoare提出使用程序公理系統(tǒng)來(lái)驗(yàn)證程序的性質(zhì)。七十年代的典型程序語(yǔ)言的數(shù)學(xué)理論并不涉及程序的規(guī)范說(shuō)明，因此不能用于軟件的設(shè)計(jì)和開(kāi)發(fā)。同時(shí)期的工作包括著重于程序性質(zhì)的后驗(yàn)證的方法，被用于一些常用算法的分析與正確性證明，但缺乏支持規(guī)范分析和指導(dǎo)安全軟件設(shè)計(jì)的演算技術(shù)。長(zhǎng)期以來(lái)國(guó)際上不少軟件公司投入了大量的人力、物力和財(cái)力探索軟件設(shè)計(jì)可靠性技術(shù)。設(shè)計(jì)嚴(yán)格安全軟件系統(tǒng)需要解決下述二項(xiàng)關(guān)鍵技術(shù)問(wèn)題:●建立程序和軟件規(guī)范的演算系統(tǒng)，在軟件開(kāi)發(fā)生命周期各階段均使用數(shù)學(xué)演算技術(shù)來(lái)建立軟件設(shè)計(jì)和開(kāi)發(fā)文檔?！裨O(shè)計(jì)完整的演算法則用來(lái)指導(dǎo)下述關(guān)鍵開(kāi)發(fā)任務(wù)：（a）從用戶需求導(dǎo)出軟件系統(tǒng)各部件的規(guī)范說(shuō)明；（b）從部件的規(guī)范說(shuō)明演算出低層軟件模塊過(guò)程的功能說(shuō)明。在軟件設(shè)計(jì)中用數(shù)學(xué)理論來(lái)指導(dǎo)嚴(yán)格安全軟件系統(tǒng)設(shè)計(jì)，包括：●同一數(shù)學(xué)框架中處理程序和軟件規(guī)范；●用符號(hào)演算實(shí)現(xiàn)程序和軟件規(guī)范間的演算；●用謂詞演算驗(yàn)證設(shè)計(jì)方法的正確性；●用代數(shù)方法從軟件部件的抽象規(guī)范說(shuō)明推算出低層次程序模塊各個(gè)過(guò)程的規(guī)范說(shuō)明。學(xué)科負(fù)責(zé)人自1985年起對(duì)設(shè)計(jì)嚴(yán)格安全軟件的完備演算理論進(jìn)行了深入研究，取得了重大突破。主要?jiǎng)?chuàng)新點(diǎn)有：●演算理論強(qiáng)調(diào)了設(shè)計(jì)正確軟件的開(kāi)發(fā)方法和使用數(shù)學(xué)演算來(lái)支持從軟件到程序代碼的轉(zhuǎn)換；●首先提出程序分解算式并第一次提出了求解規(guī)范方程的演算法則；●首次給出程序設(shè)計(jì)語(yǔ)言的一套完備的代數(shù)定律；●首先給出并證明由抽象數(shù)據(jù)類型產(chǎn)生具體數(shù)據(jù)類型的完備演算法則；●首次為海量并行程序語(yǔ)言BSP語(yǔ)言建立指稱語(yǔ)義和代數(shù)轉(zhuǎn)化方法。主要學(xué)術(shù)成果包括：●首次建立規(guī)范的數(shù)學(xué)模型，并發(fā)現(xiàn)求解規(guī)范方程(X;Q)>S和(P;X)>S的演算法則；●創(chuàng)建基于“上下仿真映照對(duì)”數(shù)據(jù)精化完備理論；●創(chuàng)建程序代數(shù)(He-Hoare代數(shù))，并用它來(lái)支持編譯器原型的設(shè)計(jì)和證明；●提出編程統(tǒng)一理論和連接各類程序理論的數(shù)學(xué)法則。軟件演算理論和數(shù)據(jù)精化規(guī)則被譽(yù)為是面向模型軟件開(kāi)發(fā)的一個(gè)里程碑，是國(guó)際標(biāo)準(zhǔn)規(guī)范語(yǔ)言Z的精化理論基礎(chǔ)，是歐洲系統(tǒng)設(shè)計(jì)語(yǔ)言B的軟件開(kāi)發(fā)方法的理論及基礎(chǔ)。學(xué)科負(fù)責(zé)人還參與了包括歐共體“硬件編譯器”項(xiàng)目在內(nèi)的若干提前一年完成。在工業(yè)界，模擬很大程度上被認(rèn)為與驗(yàn)證是同義的，設(shè)計(jì)過(guò)程經(jīng)常遵循由規(guī)范得到實(shí)現(xiàn)的過(guò)程，二者可通過(guò)一系列的輸入來(lái)進(jìn)行模擬，模擬可以重復(fù)進(jìn)行，這樣，錯(cuò)誤之處將得以發(fā)現(xiàn)、改正。1993年至1996年，學(xué)科負(fù)責(zé)人與Intel公司硬件驗(yàn)證小組和Cornell大學(xué)合作，設(shè)計(jì)了一個(gè)硬件編譯器。這類源語(yǔ)言的特征是：(1)對(duì)通過(guò)同步信息傳送的并行進(jìn)程、通訊作了明確的描述；(2)非常自然地描述數(shù)字系統(tǒng)。這個(gè)項(xiàng)目展示了怎樣使用“握手模式的規(guī)范”來(lái)為延時(shí)不敏感電路和時(shí)鐘電路產(chǎn)生一套等價(jià)的規(guī)格說(shuō)明。一個(gè)自動(dòng)工具被用于檢查“低層的實(shí)現(xiàn)是否符合了它們的規(guī)范”。該研究結(jié)果表明，應(yīng)著重考慮在一個(gè)給定的系統(tǒng)中建立概念間的聯(lián)系，這種聯(lián)系在于：(a)狀態(tài)圖(用來(lái)描術(shù)基本電路的行為)；(b)延時(shí)不敏感代數(shù)(Delay-InsensitiveAlebraic)(用來(lái)詳細(xì)說(shuō)明延時(shí)不敏感電路)；(c)通訊序列進(jìn)程(用來(lái)描述通訊界面)；(d)時(shí)鐘進(jìn)程代數(shù)(用來(lái)描述同步電路)；(e)控制和數(shù)據(jù)界面(用來(lái)將控制模式和數(shù)據(jù)模式聯(lián)系起來(lái))間的關(guān)系，這清楚地說(shuō)明了要一個(gè)統(tǒng)一構(gòu)架來(lái)處理不同范式、概念間的界面的迫切性。過(guò)去幾年里，學(xué)科負(fù)責(zé)人在微處理器驗(yàn)證方面也作了一些成功的工作，有些工作采用HOL(即HighOrderLogic)系統(tǒng)，有些工作以“功能演算”和“抽象狀態(tài)機(jī)”為基礎(chǔ)，不管怎樣，形式化方法始終不能替代已有的模擬方法。所需要的一種方法，是使設(shè)計(jì)過(guò)程能以形式化技術(shù)為基礎(chǔ)，但所包含的模擬過(guò)程能使設(shè)計(jì)形象化，有助于系統(tǒng)的開(kāi)發(fā)。形式化的規(guī)則被引用進(jìn)來(lái)，能幫助硬件工程師更正確地計(jì)算參數(shù)，考慮設(shè)計(jì)細(xì)節(jié)，為工程判斷上的決策提供方法。這種將形式語(yǔ)義和可驗(yàn)證的模擬器組合起來(lái)的方法將為工程設(shè)計(jì)帶來(lái)更高的可靠性。解決仿真與合成的不一致性是關(guān)鍵問(wèn)題。在軟硬件混合系統(tǒng)設(shè)計(jì)的不同階段所使用的系統(tǒng)語(yǔ)言是不同的。在需求分析階段，時(shí)段邏輯語(yǔ)言和通訊進(jìn)程代數(shù)會(huì)用來(lái)描寫系統(tǒng)的實(shí)時(shí)性質(zhì)以及它和周邊環(huán)境的交互功能。設(shè)計(jì)階段會(huì)使用一個(gè)并行語(yǔ)言來(lái)實(shí)現(xiàn)需求階段所提出的函數(shù)和非函數(shù)功能，高級(jí)分解器會(huì)將這樣一個(gè)程序自動(dòng)分解為軟件子系統(tǒng)和硬件子系統(tǒng)的描寫，機(jī)器語(yǔ)言和網(wǎng)表語(yǔ)言又是軟件編譯器和硬件綜合器的目標(biāo)語(yǔ)言。為了保證設(shè)計(jì)方法的正確性，設(shè)計(jì)過(guò)程被用到的多類語(yǔ)言就必須在同一語(yǔ)義框架中加以形式化處理。這也被用來(lái)保證多類轉(zhuǎn)換器(軟硬件分析器，硬件綜合器，軟件編譯器)設(shè)計(jì)的正確性。為了支持產(chǎn)品的優(yōu)化設(shè)計(jì)，協(xié)同設(shè)計(jì)方法還得提供一套精化法則用來(lái)實(shí)現(xiàn)語(yǔ)義等價(jià)設(shè)計(jì)之間的轉(zhuǎn)換，并基于代數(shù)語(yǔ)義進(jìn)行等價(jià)性證明。在此基礎(chǔ)上，說(shuō)明仿真器的工作與形式化描述的一致性。上述這些使得系統(tǒng)設(shè)計(jì)可逐步引入多類優(yōu)化來(lái)減少物理資源的共享和控制邏輯的切換。同時(shí)，工具也是必需的。協(xié)同設(shè)計(jì)技術(shù)所使用的多類支持工具包括：系統(tǒng)性能分析工具、系統(tǒng)分解器、交互式仿真器等。這里的主要挑戰(zhàn)是設(shè)計(jì)一個(gè)軟硬件混成系統(tǒng)的統(tǒng)一語(yǔ)義框架用來(lái)處理、驗(yàn)證多類轉(zhuǎn)換系統(tǒng)的正確性。這是基于語(yǔ)義等價(jià)變換設(shè)計(jì)方法的數(shù)學(xué)基礎(chǔ)，也是構(gòu)造多類工具的邏輯基礎(chǔ)。由于在混成型系統(tǒng)設(shè)計(jì)各個(gè)階段設(shè)計(jì)人員會(huì)使用各種不同規(guī)范、編程和設(shè)計(jì)語(yǔ)言與范式，而多種文檔之間的轉(zhuǎn)換又依賴于語(yǔ)義等價(jià)轉(zhuǎn)換軟件，為這一大類語(yǔ)言設(shè)計(jì)共同的語(yǔ)義模型就成為整個(gè)設(shè)計(jì)方法的關(guān)鍵難點(diǎn)。為了減少模型的復(fù)雜性，設(shè)計(jì)方法也得建立不同的語(yǔ)言之間的連接技術(shù)和變換法則。語(yǔ)義等價(jià)性問(wèn)題是必須討論和解決的。在軟硬件混成系統(tǒng)中，硬件的并行機(jī)制是建立在共享變量和信號(hào)驅(qū)動(dòng)之上的，但軟硬件之間的交互依賴于同步通訊機(jī)制。這種統(tǒng)一的語(yǔ)義框架就不得不涉及一個(gè)面向通訊和狀態(tài)共享的混合型并行語(yǔ)言。這是在國(guó)際上還未研究過(guò)的難題。硬件設(shè)計(jì)語(yǔ)言VERILOG包含多類在軟件編程語(yǔ)言中從未使用過(guò)的結(jié)構(gòu)和語(yǔ)句，它們的形式化描述和相應(yīng)的精化法則被國(guó)際計(jì)算機(jī)界認(rèn)為是對(duì)傳統(tǒng)語(yǔ)義研究的一個(gè)挑戰(zhàn)。為了增加該工具的靈活性，除了進(jìn)行多類性能分析之外，還包括與用戶直接交互的通訊手段，這也增加了該軟件工具設(shè)計(jì)和實(shí)施的復(fù)雜性。還有一個(gè)技術(shù)難點(diǎn)涉及到軟硬件子系統(tǒng)之間的通訊界面的設(shè)計(jì)，采用傳統(tǒng)方法（同步或異步）使該部件結(jié)構(gòu)規(guī)范化，但會(huì)影響整個(gè)混成系統(tǒng)的性能，并且不利于系統(tǒng)的單芯片實(shí)現(xiàn)方案。為了增加系統(tǒng)的安全性和可移植性，本項(xiàng)目實(shí)施技術(shù)將不固定軟硬件通訊界面的協(xié)議，而根據(jù)用戶對(duì)系統(tǒng)的要求（處理速度、信息量）來(lái)設(shè)計(jì)面向應(yīng)用的專用通訊界面。在系統(tǒng)的單芯片實(shí)施方案中，界面描寫最終仍可用硬件來(lái)實(shí)現(xiàn)。在設(shè)計(jì)實(shí)時(shí)嵌入式系統(tǒng)中，由于可用的硬件資源限制（性能、功耗、面積），產(chǎn)品的優(yōu)化是一個(gè)重要課題。軟硬件轉(zhuǎn)換器和分解器設(shè)計(jì)中將結(jié)合多類分析優(yōu)化技術(shù)來(lái)減少元器件的數(shù)目，增加元器件在硬件子系統(tǒng)中的重用性。將對(duì)應(yīng)的結(jié)構(gòu)重組（Reconfigurable）也是一個(gè)技術(shù)難點(diǎn)。將為軟硬件混合系統(tǒng)的可組合描寫、分析和設(shè)計(jì)提供一個(gè)綜合性的理論框架和設(shè)計(jì)方法，它們具有下屬幾個(gè)特征：（1）它能處理多類函數(shù)和非函數(shù)的需求分析，提出模塊化和優(yōu)化的處理方案。（2）基于形式化技術(shù)，從而保證目標(biāo)產(chǎn)品的可靠性和安全性。（3）能容納多類不同開(kāi)發(fā)語(yǔ)言，并提供它們之間語(yǔ)義等價(jià)轉(zhuǎn)換的法則。與硬件系統(tǒng)設(shè)計(jì)密切聯(lián)系的軟件方面，規(guī)格說(shuō)明的形式化及相應(yīng)的開(kāi)發(fā)方法和驗(yàn)證工具還未設(shè)計(jì)出來(lái)。更進(jìn)一步講，許多現(xiàn)有的形式化方法缺乏足夠的應(yīng)用范圍，它們沒(méi)有將許多性質(zhì)(如：可靠性、安全性)進(jìn)行組合考慮。軟硬件混合系統(tǒng)關(guān)鍵挑戰(zhàn)是：為硬件、軟件的協(xié)同設(shè)計(jì)尋找一個(gè)統(tǒng)一構(gòu)架，使我們的設(shè)計(jì)能跟上“半導(dǎo)體設(shè)備及相應(yīng)軟件”復(fù)雜性的飛速增加。另外，也要求我們?cè)谶@相同的構(gòu)架內(nèi)，既要解決模擬與數(shù)字設(shè)備，同時(shí)也要解決多時(shí)鐘系統(tǒng)問(wèn)題。準(zhǔn)備采用IntervalTemporalLogic(即ITL)作為高層規(guī)范的描述工具，與其它邏輯不同，ITL既能用來(lái)描述順序系統(tǒng)，又能用來(lái)描述并行系統(tǒng)，同時(shí)ITL又強(qiáng)有力地支持工業(yè)界應(yīng)用系統(tǒng)的安全性、實(shí)時(shí)性、可靠性等性質(zhì)。由于模擬方法太花時(shí)間，最終不能絕對(duì)保證硬件設(shè)計(jì)的準(zhǔn)確性。而向?qū)嶋H工業(yè)界應(yīng)用的硬件系統(tǒng)，首先要保證準(zhǔn)確，同時(shí)又要提高開(kāi)發(fā)速度，所以要研究面向“這些工業(yè)系統(tǒng)”硬件設(shè)計(jì)的軟件開(kāi)發(fā)方法，“硬件規(guī)范”用ITL來(lái)描述，使設(shè)計(jì)的準(zhǔn)確性歸約到上述ITL公式的準(zhǔn)確性。用本學(xué)科研究提供的軟、硬件混合設(shè)計(jì)方法，對(duì)于硬件系統(tǒng)的設(shè)計(jì)而言，只要寫出相應(yīng)的軟件描述即可。學(xué)科負(fù)責(zé)人在英國(guó)工作期間已經(jīng)將這類方法使用在SONY公司的VCD穩(wěn)定器和西敏寺銀行的智能卡設(shè)計(jì)上。前者產(chǎn)品成本不到一美元，后者得到了英國(guó)工貿(mào)部LEVEL-5產(chǎn)品安全證書(shū)（最高可靠性）。無(wú)論嚴(yán)格安全軟件理論還是計(jì)算機(jī)軟硬件協(xié)同設(shè)計(jì)，均站在國(guó)際前列。三、項(xiàng)目建設(shè)目標(biāo)在嚴(yán)格安全軟件理論與數(shù)據(jù)精化法則方面：具備國(guó)際級(jí)影響；形成與歐美相當(dāng)水平的學(xué)派；培養(yǎng)出一個(gè)良好的學(xué)術(shù)梯隊(duì)；并推出計(jì)算機(jī)軟硬件協(xié)同設(shè)計(jì)平臺(tái)，為SOC(SystemOnChip)的設(shè)計(jì)提供先進(jìn)的開(kāi)發(fā)工具。這將是典型的具有原創(chuàng)性和自主知識(shí)產(chǎn)權(quán)的產(chǎn)、學(xué)、研密切結(jié)合的標(biāo)志性成果。我國(guó)SOC能力十分薄弱，在汽車、航天、家電、醫(yī)療行業(yè)和金融界等，這樣的平臺(tái)有著極為廣泛的應(yīng)用前景?，F(xiàn)在，我國(guó)研究人員往往去西方發(fā)達(dá)國(guó)家學(xué)習(xí)、訪問(wèn)。建議重點(diǎn)學(xué)科若被批準(zhǔn)，相信國(guó)外的研究人員將到這里來(lái)學(xué)習(xí)、訪問(wèn)。四、項(xiàng)目建設(shè)所需經(jīng)費(fèi)本項(xiàng)目建設(shè)總投入經(jīng)費(fèi)900萬(wàn)元，其中中央專項(xiàng)資金100萬(wàn)元（即國(guó)家計(jì)委100萬(wàn)元），上海市政府配套100萬(wàn)元，學(xué)校自籌資金（學(xué)校教育產(chǎn)業(yè)及事業(yè)收費(fèi)收入等）700萬(wàn)元。具體資金投向?yàn)椋涸O(shè)備與環(huán)境730萬(wàn)元；國(guó)際學(xué)術(shù)活動(dòng)70萬(wàn)元；學(xué)科建設(shè)資料100萬(wàn)元。本項(xiàng)目擬購(gòu)的代表性儀器設(shè)備有：SUN服務(wù)器、主要用于協(xié)同計(jì)算的IBM主機(jī)、用于科學(xué)計(jì)算的IBM小型機(jī)等。五、項(xiàng)目建設(shè)已有條件、優(yōu)勢(shì)和特點(diǎn)學(xué)科所在的軟件學(xué)院是國(guó)家35所軟件學(xué)院之一，學(xué)校、復(fù)星高科技集團(tuán)、國(guó)家外國(guó)專家局和海外銀行在政策和財(cái)力方面給予了各種支持。國(guó)家