文档介绍：第三章漏洞
注：本章内容按以下三个方面来讲，重点关注漏洞检测技术
基础概念
漏洞检测技术
漏洞分类
1、 攻击者可以做什么？
避免认证
特权升级
绕过安全检查
拒绝服务(崩溃/软管配置)
远程运行代码
2、 什么是软件漏洞？
一个软件漏洞是在规范、开发、或配置软件上的一个错误的实例，其执行可以违反(隐 式或显式)安全策略。
3、 在计算机网络中最常见的安全漏洞问题的来源？
设计缺陷
错误的实现
差劲的安全管理
社会工程
4、 ppt里面的一个小例子，这段程序的小bug,你找到了吗？哈哈哈！！
int read_packet(int fd)
(
char header[50];
char body[100];
size_t bound_a = 50;
size_t bound_b = 100;
read(fd, header, bound_b);
read(fd, body, bound_b);
return 0;
}
5、 形式化系统证明
形式化方法：基于形式化验证的自动化技术，证明系统没有漏洞，证明和先决条件必须 包括所有外部因素。实际上，就是在特定的程序、设计或环境中的证明没有缺陷。
6、形式化方法的缺点
使用门槛较高，难度较大，会给传统的程序开发人员带来巨大冲击。
形式化方法对于较小规模的项目是有效的，但却很难应用于一些大型系统。
只能证明某一个漏洞不存在，但是不能证明是否存在其他漏洞。
7、 形式化方法的优点
基于计算机的工具所支持，机器可以识别，能够实现自动化。
以逻辑精确性为特色，无二义性可以严格地证明开发的正确性。
证明一个系统符合它的规范，给程序提供更好的安全性。
8、 模型检查(直接放图！！)(注：是属于验证中的一部分，我还是按照PPT顺序先写了这个)
9、 规格化(Specification)或描述：用数学定义的语法和语义去描述系统或程序的行为性质 或非行为性质，包括：功能性行为、择时行为、性能特点、内部结构、实时约束、安全 策略等。
10、 验证(Verification)：包括两种模型检验和定理证明
模型检验：建立一个有限的系统模型，并进行一个详尽的搜索。包括：自动机模型校验和 时序模型校验。
定理证明：选定一个数学逻辑体系，并用其中的公式来描述系统和系统性质刻画公式, 然后在一定的数学逻辑体系中依据此体系的公理、定理、推导规则和系统描述公式，看看能 不能推导出系统的性质刻画公式，如果可以的话验证成功。
下面这个图是定理证明，类似于我们学过的离散数学中的逻辑！！
Notation for writing desired properties of finite-state structures
Starting point: propositional logic
-Atomic propositions
&&, ||, I (not), => (implies), etc.
-Using propositional logic you can write properties of states,
Additions: operators for talking about time
F: "eventually