odymit's blog

软件漏洞分析技术第8章定理证明读书笔记。 定理证明 基本原理 技术框架 特点 方法实现 程序转换 属性描述 定理证明 实例分析 典型工具 Saturn ESC/Java 基本原理 定理证明的基本步骤： 用逻辑的方法将系统规范的功能和性质形式化为逻辑形式的模型 将系统设计实现也形式化为逻辑形式的模型 用数学定理进行推导证明实现的模型等价于或者蕴含规范的模型 定理证明的优点： 误报率很低 可以处理无限状态空间问题 只要程序表达为规范形式，就可以进行推理验证安全属性 定理证明的缺点： 需要程序员输入额外注释 交互式定理证明系统需要与用户交互 形式化程序转化为定理表达式存在困难，并且证明推理过程过于抽象，缺乏运行过程信息 漏洞产生过程的能力较差 典型工具 Saturn：该工具的实现主要基于函数abstract，同时基于条件约束进行分析。 ESC/Java：该工具用来检测 Java 漏洞。

软件漏洞分析技术第7章模型检测读书笔记。 模型检测 基本原理 技术框架 技术特点 方法实现 程序建模 安全缺陷属性描述 程序漏洞检测 实例分析 线性时序逻辑检查 分布式软件漏洞检测 典型工具 SLAM MOPS 基本原理 模型检测（model checking）基于状态转换系统来判断程序的安全性质，基本分析步骤如下： 将软件构造为状态机等抽象模型 使用模态/时序逻辑公式等形式化表达描述安全属性 对模型进行遍历验证安全属性，判断是否存在漏洞 该方法优点有： 自动化程度高 可以检测多种属性 对有限状态系统而言，算法可终止 模型检测能够给出诊断信息 该方法的不足有： 状态空间爆炸 建模时，对时序、执行路径等安全属性边界的近似处理难度大 软件中可能存在数据无限性和控制无限性 检测对象为抽象模型，最终结果准确性取决于模型的准确性 安全缺陷属性描述 安全缺陷属性是指对实际编程开发中发现的不良变成习惯、程序逻辑错误代码等质量缺陷代码进行总结抽象，然后使用形式化语言描述建模形成用于检测的时序模式。 检测算法：模型检测算法比较多，如 labeling算法 ...

软件漏洞分析技术第6章符号执行读书笔记。 符号执行 基本原理 方法实现 实例分析 典型工具 Clang KLEE 基本原理 符号执行的分析过程如下： 将变量用符号值表示 分析程序执行流程 将变量表示为符号和变量的表达式 实现方法 符号执行存在两种分析方式： 正向分析 逆向分析 还可以使用符号执行构造测试用例。 典型工具 Clang：Clang 能够分析和编译 C、C++、Objective C++ 等语言。该工具不仅是一个静态分析工具，还是一个轻量级编译器。 KLEE：KLEE 可用于分析 Linux 系统下的 c 语言程序，在分析程序构造测试用例的同时，也可以用来对变量取值范围进行符号分析。

软件漏洞分析技术第5章读书笔记。 污点分析 基本原理 方法实现 基于数据流 基于依赖关系 实例分析 典型工具 Pixy TAJ 基本原理 污点分析的一般步骤： 识别污点信息的产生，并且标记污点信息 利用特定规则跟踪分析污点信息在程序中的传播过程 在关键点检测程序操作是否会受到污点信息的影响 基于污点分析的漏洞挖掘可以通过两种方式实现： 基于数据流的污点分析 基于依赖关系的污点分析（污点数据控制流）

软件漏洞分析第4章数据流分析读书笔记。 数据流分析 基本原理 基本概念 程序路径 流不敏感 流敏感 路径敏感 路径范围 过程内（函数内） 过程间（函数间） 检测程序漏洞 辅助支持技术 方法实现 检测 作为辅助技术 实例分析 检测 作为辅助技术 典型工具 Fortify SCA Coverity Prevent FindBugs 基本原理 在应用数据流分析直接进行漏洞检测时，可以通过词法分析、语法分析、控制流分析以及其他程序分析技术对代码进行分析，将程序代码转化为抽象语法树（abstract syntax tree, AST）、三地址码（three address code, TAC）等关键代码中间表示，并且获得程序的控制流图、调用图等数据结构。 方法实现 抽象语法树：抽象语法树是程序抽象语法结构的树状表现形式。 三地址码：三地址码类似汇编指令，有不多于三个的运算分量。 静态单赋值形式：静态单赋值形式是一种程序语句或者指令的表示形式，其代码通常是指静态单赋值形式的三地址码。 控制流图：控制流图通常是指用于描述程序过程内的控制流的有向 ...

软件漏洞分析技术漏洞分析基础部分读书笔记。 软件漏洞 漏洞 漏洞概述 漏洞定义 漏洞特点 持久性与时效性 广泛性与具体性 可利用性与隐蔽性 漏洞分类与分级 漏洞分类 早期漏洞分类 多维度漏洞分类 综合性漏洞分类 漏洞库中的漏洞分类 漏洞分级 CNNVD 微软 US-CERT CVSS 漏洞的影响 漏洞分析发展历程 漏洞分析发展历程 软件漏洞分析 广义漏洞分析 漏洞挖掘 漏洞检测 漏洞应用 漏洞消除 漏洞管控 狭义漏洞分析 特指漏洞挖掘 架构安全分析 源代码漏洞分析 二进制漏洞分析 运行系统漏洞分析 原始萌芽阶段 通信安全 分析萌芽 信息加密 初步发展阶段 计算机安全 单一化漏洞挖掘 操作系统防护 高速发展阶段 互联网安全 多样化漏洞分析 信息系统防护 综合治理阶段 网际安全 系统化漏洞管控 防御体系建设 漏洞分析技术概述 漏洞分析技术概述 漏洞分析技术体系 软件架构安全分析 形式化架构分析技术 工程化架构分析技术 源代码漏洞分析 基于中间表示的分析技术 数据流分析 符号执行 ...

主要介绍了以下操作： snmp服务的安装 snmp相关的一些简单操作 Windows下可以开启snmp服务的代理端，不过如果要进行网络管理需要安装专用的nms软件，如果是简单的操作则需要安装net-snmp或者snmputil来实现. Linux下主要使用到的软件是snmp snmpd snmp-mibs-downloader 系统信息及操作 系统信息：Linux 4.15.0-70-generic #79~16.04.1-Ubuntu SMP x86_64 本地测试 安装snmp 1sudo apt-get install snmp snmpd 查看安装版本 123456user@flyinfort:~$ snmpd -vNET-SNMP version: 5.7.3Web: http://www.net-snmp.org/Email: net-snmp-coders@lists.sourceforge.net 启动和查看snmpd服务 123456789101112131415161718user@flyin ...

mitre-attack 工具调研 调研 github 上 mitre-attack 相关的工具，目标是寻找能够把审计记录映射到 mitre-attack 对应战术和技术上的工具。 atomic-red-team 仓库链接：https://github.com/redcanaryco/atomic-red-team Atomic Red Team 是一个能够映射到 mitre-attack 框架上的测试库，安全团队可以使用该工具方便、快速地测试他们的环境。 该项目是一个用于测试的集合，以 mitre-attack 框架的编号进行分类，需要进行那一项技术的安全测试可以执行对应的测试，有较为详细的说明和代码实例，但是与现在的目标有所区别。 sysmon-modular 是面向 windows 系列的审计日志工具，因为使用 linux 系列的平台，windows 系列工具与目标不符合。 值得一提的是该项目的关于配置和 mitre-attack 的映射还是比较全的，只是暂时并不会使用 windows 系列系统作为实验环境。 ATTACK-Tools 该项目是一个 ATT&CK 相关的 ...

本文将会总结过去几篇有关 APT 攻击检测相关的论文中提到的相关工作，从而能够较为清晰地认识当前在该领域内的前人工作和前沿技术，具体会总结以下几篇论文中的相关工作： UNICORN: Runtime Provenance-Based Detector for Advanced Persistent Threats DeepHunter: A Graph Neural Network Based Approach for Robust Cyber Threat Hunting HOLMES: Real-time APT Detection through Correlation of Suspicious Information Flows ATLAS: A Sequence-based Learning Approach for Attack Investigation 威胁狩猎方法（DeepHunter） Poirot [1] 是跟 DeepHunter 相关的工作，在相关工作中提及，并在文章的 7.2 节中详细介绍后进行了性能对比。该章节中提到， Poirot 是当前威胁狩猎 ...

abstract 1Advanced Persistent Threats (APTs) are difficult todetect due to their “low-and-slow” attack patterns and frequent use of zero-day exploits. We present UNICORN, an anomaly- based APT detector that effectively leverages data provenance analysis. From modeling to detection, UNICORN tailors its design specifically for the unique characteristics of APTs. Through extensive yet time-efficient graph analysis, UNICORN explores provenance graphs that provide rich contextual and historical infor ...