《基于z规格的软件缺陷形式化方法》由会员分享，可在线阅读，更多相关《基于z规格的软件缺陷形式化方法（73页珍藏版）》请在金锄头文库上搜索。
1、基于Z 规格的软件缺陷形式化方法 F o r m a l i z i n g S o f t w a r eW e a k n e s s e sB a s e dO n Z S p e c i f i c a t i o n 学科专业：计算机应用技术 研究生：H a m z aI B a n g u r a 指导教师：李晓红教授 j 名 独创性声明 r l l l ll r l il l r I l f f I l l ll rl llllll 18 7 3 8 2 8 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含
2、其他人已经发表或撰 写过的研究成果，也不包含为获得丕盗盘鲎或其他教育机构的学位或证书而使 用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确 的说明并表示了谢意。 学位论文作者签名：字日期：钿f o 年毛月f 伯 学位论文版权使用授权书 本学位论文作者完全了解鑫盗盘鲎有关保留、使用学位论文的规定。特授 权墨盗盘堂可以将学位论文的全部或部分内容编入有关数据库进行检索，并采 用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关 部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 一躲脚翩虢西彬伊 签字日期：巾年，c 月代日签字日
3、期：冲年月何日 f I 摘要 随着软件的在关键领域如电子商务、银行、航空等的广泛应用，其可信性已经 越来越多的获得人们的关注，据报道，2 0 0 0 年至U 2 0 0 6 年基于W E B 的攻击从2 5 上 涨到6 1 。然而，目前的软件工程方法无法有效的保障软件的可信性，针对软件成 品的测试能够一定程度的保证软件的安全性、可靠性，但该过程依赖于测试人员的 能力、经验、状态等一系列不确定因素，同时，对于设计阶段引入的缺陷，其缓和 成本过高。C W E 网站对目前已知的软件安全缺陷进行了总结与整理，然而其描述 是基于自然语言的，缺乏足够的语义信息，计算机不能够自动识别并处理。 本毕设对软件设
4、计阶段引入的安全缺陷进行了总结、抽象、形式化，并通过Z 语言对其进行了形式化的描述，建模了软件安全缺陷发生的本质及可能的缓和方 案。基于上述结构，构建了基于本体的软件安全缺陷知识库，作为软件安全专家系 统的核心部分，为缺陷的形式化验证、软件的安全性评估及其他相关工具的开发奠 定了坚实的基础。最后，通过网上银行案例，验证了上述理论的正确性及有效性， 同时，结合统一软件模型，实现了基于定理证明的软件安全性形式化验证。 综上所述，本毕设实现了软件可信工程中，设计阶段的软件安全性验证，同 时，软件安全缺陷知识库为其他研究组织提供了结构定义完善的软件安全缺陷信 息。 关键字：软件安全缺陷；z 规格；知识
5、库；形式化方法 A B S T R A C T T h i st h e s i sp r e s e n t sas t u d yo ft h ef o r m a l i z a t i o no fs o f t w a r ew e a k n e s s e sb a s e do nZ s p e c i f i c a t i o n s T h r o u g hd e e p l ye x p l o r i n gt h ec h a r a c t e r i s t i c so fs o f t w a r ew e a k n e s s e s 。I d e v
6、 e l o pak n o w l e d g eD a t a b a s el e v e r a g i n gt h ec o n c e p t so fO n t o l o g ye n g i n e e r i n g W i t h t h ei n c r e a s i n go ft h ec o m p l e x i t yo fS o f t w a r ed e v e l o p m e n t ，i ti sm o r ea n dm o r ei m p o r t a n t t ou n d e r s t a n dt h e h i g h -
7、 l e v e li m p a c t s o fw e a k n e s s e s P r o t o t y p i n ga n dd e s c r i b i n g w e a k n e s s e sa r et w om e a n so fv a l i d a t i 0 1 1 H o w e v e r , n e i t h e rg i v e sf u l la s s u r a n c et h a ta l l p o s s i b l es i t u a t i o n sh a v eb e e nt h e e k e da n dt h
8、 es y s t e ma l w a y sw o r k sa se x p e c t e d F u r t h e r m o r e ，c o m p a r e d w i t h i n c r e a s i n go fd e s i g nc o m p l e x i t y , t h ep e r c e n t a g eo f w e a k n e s s e sr e p o r t e di s r a p i d l yi n c r e a s i n ga t af a s t e r r a t e I ti s r e p o r t e dt
9、 h a t ，t h e p e r c e n t a g eo fw e b b a s e da t t a c k sr o s ef r o m2 5 o ft h et o t a ln u m b e ro fe n t r i e si n2 0 0 0t o 6 1 i n2 0 0 6 A n dm o s to f t h e s es e c u r i t yi s s u e sa l ec a u s e db yt h ed e s i g nl e v e lf l a w s S o l v i n gt h e s ep r o b l e m sn e
10、 e d sc o n c r e t ei n f o r m a t i o nt ob e t t e ru n d e r s t a n d si t sp o t e n t i a l t h r e a t st h a th e l pi n d i v i d u a ll a yc l e a rs t r a t e g i e sf o rm i t i g a t i o n s T h e r e f o r e ，Iu s et h eC 、E w e b s i t ea sag u i d i n gt o o lf o rs u c hi n f o r
11、m a t i o na sc u r r e n t l yh o s tal o to fs e c u r i t y i n f o r m a t i o na n dt h a ti m p o r t a n t l yr e d u c e sc o s t B u tn o t w i t h s t a n d i n gt h i sf a c t t h eC 、E w e b s i t eu s e san a t u r a ll a n g u a g et od e s c r i b ew e a k n e s s e sa n dt h e r e f
12、o r el a c k sa d e q u a t e s e m a n t i ci n f o r m a t i o nt ob eu n c l e r s t o o db yas y s t e mo ru s e db yap r o g r a n 】Ih a v eu s e d f o r m a lm e t h o d st od e s c r i b et h e s ew e a k n e s s e sa n dt h u si n c l u d e ：U s i n gm a t h e m a t i c a l f o r m u l a t i
13、 o nt od e s c r i b ew e a k n e s s e s a p p l y i n gZl a n g u a g et oi m p r o v et h ef o r m a l i z a t i o n p r o c e s sa n dt h e nb u i l d i n g aK n o w l e d g eD a t a b a s et h a tw i l lb eu s e db Yp r o g r a m sa n d e x p e r ts y s t e m s M yw o r kw i l lc o n t r i b u
14、t e t o m a k i n gp r o g r a m s a n de x p e r ts y s t e m s u n d e r s t a n dm o r ea b o u tw e a k n e s s e s T h ee f f e c t i v e n c s sa n dt h ep r a c t i c a lu s e f u l n e s so ft h e a p p r o a c ha r ee x e m p l i f i e db ya ni l l u s t r a t i v eO n l i n eb a n k i n gs
15、 c e n a r i ot od e t e c tw e a k n e s s e s K E Y W o R D S ：S o f t w a r eW e a k n e s s e s ；ZS p e c i f i c a t i o n s ；K n o w l e d g eD a t a b a s e ； F o r m a lM e t h o d C o N T E N T S C o N l E N r S 1 C h a p t e rIB a c k g r o u n d 1 1 1P r o b l e mD e f m i t i o na n dM o t i v a t i o n 2 1 ：! I ) b i e c t i v e s ：3 1 3A r e ao f C o n t r i b u t i o n 3 1 4T h e s i sS t r u c t u r e 4 C h a p t e rI IR e l a t e dW o r k 6
