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

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

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

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