基于UMLsec的系統(tǒng)安全模型的形式化與檢測(cè).pdf

1、由設(shè)計(jì)瑕疵引起的安全問題占據(jù)了系統(tǒng)開發(fā)過程中出現(xiàn)的安全性問題的50％，因此，無論在多么堅(jiān)實(shí)的軟件安全程序中，對(duì)于系統(tǒng)體系結(jié)構(gòu)的風(fēng)險(xiǎn)分析都顯得十分重要。安全性風(fēng)險(xiǎn)分析是一種將技術(shù)問題和數(shù)據(jù)考量等相聯(lián)系的自然方法，是在軟件系統(tǒng)開發(fā)生命周期的初期階段就需要完成的步驟。安全風(fēng)險(xiǎn)分析的結(jié)果和風(fēng)險(xiǎn)類別同時(shí)也驅(qū)動(dòng)了軟件安全性需求分析和安全性測(cè)試。
　　 系統(tǒng)安全性需求分析與建模是將風(fēng)險(xiǎn)分析的過程放在了軟件生命周期的早期需求層，這是進(jìn)行軟件體系

2、結(jié)構(gòu)風(fēng)險(xiǎn)分析的最佳選擇?，F(xiàn)有的軟件安全分析與建模方法主要包括:創(chuàng)建安全對(duì)象及分析評(píng)估故障樹;在軟件生命周期的整個(gè)過程中跟蹤關(guān)鍵安全需求;在軟件質(zhì)量模型基礎(chǔ)上添加安全標(biāo)準(zhǔn)和度量等。而這些方法和模型與傳統(tǒng)的軟件設(shè)計(jì)模型存在一定差異。系統(tǒng)的安全模型往往需要進(jìn)行嚴(yán)格的形式化分析與驗(yàn)證，因此有必要使用更為嚴(yán)格的過程管理及形式化的設(shè)計(jì)與分析方法對(duì)軟件安全性進(jìn)行驗(yàn)證。
　　 使用Unified Modeling Language(UML)統(tǒng)一

3、建模語言來對(duì)軟件系統(tǒng)進(jìn)行建模是現(xiàn)在最流行的建模方式，但是對(duì)于要求嚴(yán)格的系統(tǒng)安全模型，有必要對(duì)UML建立的模型進(jìn)行形式化來分析其可行性。論文在自動(dòng)機(jī)理論基礎(chǔ)上提出了描述UML視圖的形式化機(jī)制，并將其映射到模型語言Promela，從而實(shí)現(xiàn)對(duì)使用UML建立的軟件安全模型的形式化，使得由非形式化的UML語言建立的軟件安全模型能夠得到更清晰嚴(yán)格的描述。過程中使用線性時(shí)序邏輯語言LTL定義軟件安全屬性，描述直觀并具有良好的兼容性。最后以形式化后的模