教材 P239，11 题
综合实验：用 Find Security Bugs （http://find-sec-bugs.github.io）工具静态分析 WebGoat。WebGoat 是 OWASP 组织研制出的用于进行 Web 漏洞实验的应用平台，官方网址是 http://www.owasp.org.cn/owasp-project/webscan-platform。WebGoat 运行在带有 Java 虚拟机的平台之上，当前提供的训练课程有 30 多个，其中包括：跨站点脚本攻击（XSS）、访问控制、线程安全、操作隐藏字段、操纵参数、弱会话 Cookie、SQL 盲注、数字型 SQL 注入、字符串型 SQL 注入和 Web 服务等。完成实验报告。
1 | |
教材 P239，15 题
综合实验：使用 American Fuzzy Lop（http:/lcamtuf.coredump.cx/afl/）工具挖掘 C/C++程序漏洞。完成实验报告。
实验环境：WSL2
1 | |
RAG-arXiv 实验开源地址：https://github.com/EagleBear2002/RAG-arXiv
Agent-course 实验开源地址：https://github.com/EagleBear2002/Agent-course
\[ \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\postfix{\mathsf{postfix}} \def\ww{\mathsf{ww}} \def\rw{\mathsf{rw}} \def\wr{\mathsf{wr}} \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}} \def\C{\mathrm{C}} \]
摘要
众所周知，许多数据库系统提供的隔离级别多版本读取已提交 (RC) 会牺牲一致性来换取更高的事务吞吐量。有时，事务工作负载可以在 RC 下安全执行，以较低的 RC 成本获得完美的可序列化隔离。为了识别这种情况，我们引入了一个事务程序的表达模型，以更好地推理事务工作负载的可序列化性。我们开发了易处理的算法来决定在 RC 下执行的工作负载的任何可能调度是否可序列化（称为稳健性问题）。我们的方法产生的稳健子集比以前的方法识别的子集更大。我们提供实验证据表明，与更强的隔离级别相比，在 RC 下可以更快地评估对 RC 具有稳健性的工作负载。我们讨论了通过将选择性读取操作提升为更新来使工作负载对 RC 具有稳健性的技术。根据场景的不同，性能改进可能相当可观。因此，在较低的隔离级别 RC 下进行稳健性测试和安全地执行事务可以提供一种直接的方法来增加事务吞吐量，而无需更改 DBMS 内部结构。
作者：
\[ \def\put{\mathrm{put}} \def\get{\mathrm{get}} \def\rem{\mathrm{rem}} \def\inv \def\ret \def\hb \def\lin \]
摘要
多线程程序通常依赖高效且线程安全的并发对象，如集合、键值映射和队列。虽然一些并发对象的操作被设计为原子性行为，见证其在线性化顺序中的前驱操作的原子效果，但其他操作为了避开复杂的控制和同步瓶颈而放弃了这种强一致性。例如，键值映射的
contains(value)
方法可能在不阻塞并发更新的情况下遍历键值条目，以避免不必要的性能瓶颈，因此可能会忽略某些在线性化顺序上的前驱操作的效果。尽管这些弱一致性的操作可能不具备原子性，但它们仍然提供了一些保证，比如只观察到已经存在的值。
在这项工作中，我们开发了一种方法来证明并发对象实现遵循弱一致性规范。特别是，我们考虑了对放宽可见性规范的（前向）模拟证明，允许指定的操作忽略它们的一些线性化顺序上的前驱操作，即表现得好像这些操作从未发生过一样。除了标注实现代码以识别逻辑效应发生的点（即操作的线性化点），我们还标注代码以识别可见操作，即那些效果被观察到的操作；实际上，这种标注可以通过跟踪每个访问内存位置的写入者自动完成。我们在一个通用的状态转换系统概念上形式化了我们的方法论，该概念独立于任何特定的编程语言或内存模型，并展示了其应用。
\[ \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\hbs{\mathsf{hbs}} \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 对象提供更强的规格说明。
作者：
摘要
本文记录了南京大学师生免费领取华为云云主机的步骤，以供参考。
摘要
商业数据库支持不同的隔离级别，以允许程序员在一致性和性能提升之间做出权衡。隔离级别在当前的 ANSI 标准中定义，但定义含糊不清，而为纠正该问题而提出的修订定义过于受限，因为它们仅允许悲观（锁定）实现。本文介绍了 ANSI 级别的新规范。我们的规范是可移植的；它们不仅适用于锁定实现，还适用于乐观和多版本并发控制方案。此外，与早期的定义不同，我们的新规范在所有级别上以正确且灵活的方式处理谓词。
本文给出了 ANSI-SQL 隔离级别的新、精确定义 [6]。与以前的提案 [13、6、8] 不同，新定义既正确（它们排除了所有不良历史记录），又独立于实现。我们的规范允许使用各种并发控制技术，包括锁定、乐观技术 [20、2、5] 和多版本机制 [9、24]。因此，它们符合 ANSI-SQL 的目标，可以用作隔离标准。
隔离级别的概念最初是在 [13] 中以一致性程度的名称引入的。这项工作的目标是通过牺牲完全隔离的保证来为工作负载提供更好的并发性。[13] 中的工作和 [11] 建议的一些改进为 ANSI/ISO SQL-92 隔离级别定义 [6] 奠定了基础，其目标是制定一个独立于实现的标准。然而，后续论文 [8] 表明 [6] 中提供的定义含糊不清。该论文提出了避免歧义问题的不同定义，但如 [8] 所述，这些定义只是“锁定的伪装版本”，因此不允许乐观和多版本机制。因此，这些定义未能满足 ANSI-SQL 关于实现独立性的目标。
摘要
数据异常尚没有统一的定义, 其含义是指可能破坏数据库一致性状态的特定数据操作模式. 已知的数据异常有脏写、脏读、不可重复读、幻读、丢失更新、读偏序和写偏序等. 为了提高并发控制算法的效率, 数据异常也被用于定义隔离级别, 采用较弱的隔离级别以提高事务处理系统的效率. 体系化地研究了数据异常以及对应的隔离级别, 发现了 22 种未被其他文献报告过的新的数据异常, 并对全部数据异常进行分类. 基于数据异常的分类, 提出了新的且不同粒度的隔离级别体系, 揭示基于数据异常定义隔离级别的规律, 使得对于数据异常和隔离级别等相关概念的认知可以更加简明.
