网络攻防复习第三章漏洞.docx

网络攻防复习第三章漏洞.docx第三章漏洞注:本章内容按以下三个方面来讲,重点关注漏洞检测技术基础概念漏洞检测技术漏洞分类1、 攻击者可以做什么?避免认证特权升级绕过安全检查拒绝服务(崩溃/软管配置)远程运行代码2、 什么是软件漏洞?一个软件漏洞是在规范、开发、或配置软件上的一个错误的实例,其执行可以违反(隐式或显式)安全策略。3、 在计算机网络屮最常见的安全漏洞问题的來源?设计缺陷错误的实现旁劲的安全管理社会工程4、 ppt里面的一个小例了,这段程序的小bug,你找到了吗?哈哈哈!!intread_packet(intfd){charheader[50];charbody[100];size_tbound_a=50;sizetboundb=100;read(fd,header,bound_b);read(fd,body,bound_b);return0;}5、 形式化系统证明形式化方法:基于形式化验证的自动化技术,证明系统没有漏洞,证明和先决条件必须包括所冇外部因素。实际上,就是在特定的程序、设计或环境中的证明没冇缺陷。6、形式化方法的缺点使用门槛较高,难度较大,会给传统的程序开发人员带来巨大冲击。形式化方法对于较小规模的项目是有效的,但却很难应用于一些大型系统。只能证明某一个漏洞不存在,但是不能证明是否存在英他漏洞。7、 形式化方法的优点基于计算机的工具所支持,机器可以识别,能够实现H动化。以逻辑精确性为特色,无二义性可以严格地证明开发的止确性。证明一个系统符合它的规范,给程序提供更好的安全性。8、 模型检杳(肓接放图!!)(注:是属于验证屮的一部分,我还是按照PPT顺序先写了这个)9、规格化(Specification)或描述:用数淫定义的语法和语义去描述系统或程序的行为性质或非行为性质,包括:功能性行为、择时行为、性能特点、内部结构、实时约束、安全策略等。10>验证(Verification):包括两种模型检验和定理证明模型检验:建立一个有限的系统模型,并进行一个详尽的搜索。包括:自动机模型校验和时序模型校验。定理证明:选定一个数学逻辑体系,并用其中的公式来描述系统和系统性质刻画公式,然后在一定的数学逻辑体系中依据此体系的公理、定理、推导规则和系统描述公式,看看能不能推导出系统的性质刻画公式,如果可以的话验证成功。下面这个图是定理证明,类似于我们学过的离散数学中的逻辑!!Notationforwritingdesiredpropertiesoffinite-statestructuresStartingpoint:propositionallogic一Atomicpropositions&&.||v!(not),n(implies),,Additions:operatorsfortalkingabouttimeF:Meventuall/G:'always”Note-Thereareseveralvariantsoftemporallogic-pleteness:weareusingTinear-timen例子:G(idlel11idle2)“Itisalwaysthecasethatprocess1orprocess2isidlingnG(idlelFexecl