EagleBear2002 的博客

RAG-arXiv 实验开源地址：https://github.com/EagleBear2002/RAG-arXiv

Agent-course 实验开源地址：https://github.com/EagleBear2002/Agent-course

摘要

1. 什么是软件漏洞？软件漏洞与软件错误或软件缺陷的关系是什么？
2. 为什么会出现软件漏洞？
3. 软件漏洞为什么要管理？如何管理？

什么是软件漏洞？

对信息安全中“漏洞”的认识

ISO/IEC 15408-1《信息技术—安全技术—IT 安全评估标准》：漏洞是存在于评估对象中的、在一定的环境条件下可能违反安全功能要求的弱点。

摘要

1. 什么是缓冲区溢出漏洞？
2. 什么是栈溢出？栈溢出漏洞如何利用？
3. 什么是堆溢出？堆溢出漏洞如何利用？
4. 什么是格式化字符串漏洞？该漏洞如何利用？
5. 针对缓冲区溢出漏洞，Windows 平台设置了哪些保护机制？

什么是缓冲区溢出漏洞？

内存结构

Win32 系统中，进程使用的内存按功能可以分 4 个区域

\[ \def\ReadSet{\mathsf{ReadSet}} \def\WriteSet{\mathsf{WriteSet}} \def\Attr{\mathsf{Attr}} \def\Account{Account} \def\Savings{Savings} \def\Checking{Checking} \def\Balance{Balance} \def\Amalgamate{Amalgamate} \def\Var{\mathsf{Var}} \def\Tuples{\mathsf{Tuples}} \def\prefix{\mathsf{prefix}} \def\pcfg{\mathsf{prefix-conflict-free-graph}} \def\R{\mathsf{R}} \def\W{\mathsf{W}} \def\U{\mathsf{U}} \def\t{\mathsf{t}} \def\v{\mathsf{v}} \def\T{\mathcal{T}} \def\P{\mathcal{P}} \def\D{\mathrm{D}} \]

摘要

众所周知，许多数据库系统提供的隔离级别多版本读取已提交 (RC) 会牺牲一致性来换取更高的事务吞吐量。有时，事务工作负载可以在 RC 下安全执行，以较低的 RC 成本获得完美的可序列化隔离。为了识别这种情况，我们引入了一个事务程序的表达模型，以更好地推理事务工作负载的可序列化性。我们开发了易处理的算法来决定在 RC 下执行的工作负载的任何可能调度是否可序列化（称为稳健性问题）。我们的方法产生的稳健子集比以前的方法识别的子集更大。我们提供实验证据表明，与更强的隔离级别相比，在 RC 下可以更快地评估对 RC 具有稳健性的工作负载。我们讨论了通过将选择性读取操作提升为更新来使工作负载对 RC 具有稳健性的技术。根据场景的不同，性能改进可能相当可观。因此，在较低的隔离级别 RC 下进行稳健性测试和安全地执行事务可以提供一种直接的方法来增加事务吞吐量，而无需更改 DBMS 内部结构。

作者：

• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium
• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium

\[ \def\put{\mathrm{put}} \def\get{\mathrm{get}} \def\rem{\mathrm{rem}} \def\inv \def\ret \def\hb \def\lin \]

摘要

多线程程序通常依赖高效且线程安全的并发对象，如集合、键值映射和队列。虽然一些并发对象的操作被设计为原子性行为，见证其在线性化顺序中的前驱操作的原子效果，但其他操作为了避开复杂的控制和同步瓶颈而放弃了这种强一致性。例如，键值映射的 contains(value) 方法可能在不阻塞并发更新的情况下遍历键值条目，以避免不必要的性能瓶颈，因此可能会忽略某些在线性化顺序上的前驱操作的效果。尽管这些弱一致性的操作可能不具备原子性，但它们仍然提供了一些保证，比如只观察到已经存在的值。

在这项工作中，我们开发了一种方法来证明并发对象实现遵循弱一致性规范。特别是，我们考虑了对放宽可见性规范的（前向）模拟证明，允许指定的操作忽略它们的一些线性化顺序上的前驱操作，即表现得好像这些操作从未发生过一样。除了标注实现代码以识别逻辑效应发生的点（即操作的线性化点），我们还标注代码以识别可见操作，即那些效果被观察到的操作；实际上，这种标注可以通过跟踪每个访问内存位置的写入者自动完成。我们在一个通用的状态转换系统概念上形式化了我们的方法论，该概念独立于任何特定的编程语言或内存模型，并展示了其应用。

Introduction

\[ \def\Th{\mathrm{Th}} \def\Cn{\mathrm{Cn}} \def\Mod{\mathrm{Mod}} \def\A{\mathfrak{A}} \def\B{\mathfrak{B}} \def\N{\mathfrak{N}} \def\K{\mathcal{K}} \def\lh{\mathrm{lh}} \]

本节知识点

教材 3.3 数论的子理论

习题 1：证明：在结构 \(( \mathbb{N}; \cdot, E)\) 中，我们能够定义加法关系 \(\set{\langle m, n, m+n\rangle | m, n \in \mathbb{N}}\)。进一步证明在结构 \(\set{0}\) 中，序关系 \(<\)，后继关系 \(\set{\langle n, S(n) \rangle | n \in \mathbb{N}}\) 都是可定义的。(说明：如果把结构 \(( \mathbb{N}; \cdot, E)\) 简化为 \(( \mathbb{N}; E)\), 这个结果还能加强。在此处，乘法关系可以通过指数运算的一个法则: \((d^a)^b = d^{ab}\) 来定义。）

证明：在算数关系中，很容易使用对数将乘法转化为加法。例如 \(\log(nm) = \log(n) + \log(m)\)。利用这一思路，定义加法关系为 \(\set{\langle n, m, p\rangle | 2En \cdot 2Em = 2Ep}\)，其中 \(2 = S^20\)。

在结构 \(\set{0}\) 中，定义序关系为 \(\set{\langle n, m\rangle | \exists x (x + x \neq x \land n + x = m)}\)；

在算数关系中，后继可以用 \(m = n+1\) 表示，只要构造 \(x=1\) 即可。

定义后继关系为 \(\set{\langle n, m\rangle | \exists x (x + x \neq x \land \forall y \forall z (y+y\neq y \to z+z \neq z \to y+z\neq x) \land n + x = m)}\)。

\(Q.E.D.\)

\[ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\soo{\mathsf{\textcolor{purple}{soo}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \def\AR{\mathsf{\textcolor{pink}{AR}}} \def\vis{\mathsf{\textcolor{orange}{vis}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\hb{\mathsf{\textcolor{pink}{hb}}} \def\hbo{\mathsf{\textcolor{pink}{hbo}}} \def\A{\mathsf{A}} \def\E{\mathsf{E}} \def\cc{\mathsf{cc}} \def\ec{\mathsf{ec}} \def\sc{\mathsf{sc}} \def\rc{\mathsf{rc}} \def\mav{\mathsf{mav}} \def\rr{\mathsf{rr}} \def\sameobj{\mathsf{sameobj}} \def\oper{\mathsf{oper}} \def\txn{\mathsf{txn}} \def\sametxn{\mathsf{sametxn}} \def\withdraw{\mathtt{withdraw}} \def\deposit{\mathtt{deposit}} \def\getBalance{\mathtt{getBalance}} \def\heta{\hat{\eta}} \def\RYW{\mathbf{RYW}} \def\MR{\mathbf{MR}} \def\MW{\mathbf{MW}} \def\WFR{\mathbf{WFR}} \]

摘要

面向用户的在线服务采用地理分布的数据存储来减少延迟并容忍部分故障，以提供快速且始终可用的体验。然而，地理分布并非没有代价；应用程序开发者需要处理弱一致性行为，并且缺乏构建高级复制数据类型的抽象机制，这导致了复杂的应用程序逻辑，并不可避免地将不一致性暴露给用户。一些商业分布式数据存储和多个学术提案提供了一致性级别的层次结构，更强的一致性保证会带来更高的延迟和吞吐量成本。然而，正确为操作分配合适的一致性级别需要细致的推理，并且通常是一个容易出错的任务。

在本文中，我们提出了 QUELEA，一种针对最终一致性的数据存储（ECDS）的声明式编程模型，它配备了一种契约语言，能够指定细粒度的应用层一致性属性。一个契约执行系统分析这些契约，并自动生成受保护方法所需的一致性协议。我们在一个现成的支持无协调事务的 ECDS 之上实现了 QUELEA。通过包括两个大型网络应用在内的几个基准测试，展示了我们的方法的有效性。

关键词：最终一致性、可用性、CRDT、公理合约、合约分类、分布式事务、SMT 求解器、可判定逻辑、Quelea、Cassandra、Haskell

\[ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \]

摘要

有效的软件规格说明能够支持模块化推理，允许客户端在不了解模块实现细节的情况下建立程序属性。虽然一些模块的操作表现得像原子操作一样，但其他模块为了提高性能而采用了较弱的一致性。由于当前的方法无法捕捉到具有不同非原子一致性水平的操作所提供的保证，因此规格说明变得无效，失去了为调用非原子操作的程序建立属性的能力。

在这项工作中，我们开发了一种方法来指定那些操作满足多个不同一致性级别的软件模块。特别是，我们开发了一个简单的注释语言，通过可见性放松来指定弱一致性操作，在这种注释中对操作之间的可见性施加了不同的约束。为了与现代软件平台集成，我们识别了一种新的称为“顺序发生前一致性”的一致性特性，它允许有效验证。实验上，我们通过推导和验证 Java 并发对象的放松可见性规格说明，展示了我们方法的有效性。此外，我们还通过实验证明了我们的注释语言是优化的，即使更细粒度的语言也不能为 Java 对象提供更强的规格说明。

INTRODUCTION

\[ \def\Th{\mathrm{Th}} \def\Cn{\mathrm{Cn}} \def\Mod{\mathrm{Mod}} \def\A{\mathfrak{A}} \def\B{\mathfrak{B}} \def\N{\mathfrak{N}} \def\K{\mathcal{K}} \]

本节知识点

理论是逻辑蕴涵意义下封闭的句子集合，\(T\) 是一个理论当且仅当 \(T\) 是一些句子的集合，该集合使得语言中的任意句子 \(\sigma\)， \[ T \models \sigma \Rightarrow \sigma \in T \] 注意：我们仅指句子，而不是带有自由变量的公式。

对语言的结构类 \(\K\)，定义其理论为（记作 \(\Th \ \K\)） \[ \Th \ \K = \set{ \sigma | \sigma \ 在 \ \K \ 的每个元素中都是真的} \] 这一概念由先前的特殊情况 \(\K = \set{\A}\) 而来。

对于句子集合 \(\Sigma\)，定义 \(\Mod \ \Sigma\) 为 \(\Sigma\) 所有模型的类。\(\Th \ \Mod \ \Sigma\) 则是在 \(\Sigma\) 的所有模型中都是真的的所有句子的集合。称此集合为 \(\Sigma\) 的推论集，记作 \(\Cn \ \Sigma\)，这样 \[ \Cn \Sigma = \set{\sigma | \Sigma \models \sigma} \\ = \Th \ \Mod \ \Sigma \] 一个句子集合是一个理论当且仅当 \(T = \Cn \ T\)。

摘要

本文记录了南京大学师生免费领取华为云云主机的步骤，以供参考。

领取步骤

1. 手机下载“华为云 APP”并注册、登录；
2. 使用“华为云 APP”扫描文档中的二维码（本文不提供二维码）；
3. 自动跳转云主机领取配置页面（这一步骤需要时间，请耐心等待）；