并发系统审计日志记录的正确实现模型及算法研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）115-141www.elsevier.com/locate/entcs并发系统中的正确审计日志记录Sepehr Amir-Mohammadiana，1 Chadi Karia，2a太平洋大学工程与计算机科学学院，Stockton，California 95211摘要审计日志记录为不同的目的提供了运行时行为的事后分析，包括错误检测、系统操作的改进以及深度安全性的建立。这需要对生成的审计日志的质量有一定程度的保证，即，审核日志对执行过程中发生的事件的描述程度。信息代数技术已被提出来正式指定这种关系，并提供了一个框架，以研究正确的审计日志生成的可证明的方式。然而，以前的工作缺乏如何在并发环境中保证审计日志的这种属性。在本文中，我们研究了在并发环境中的实现模型。 我们提出了一种算法，仪器的并发系统根据审计日志要求的正式规范，使任何仪器并发系统保证正确的审计日志生成。作为一个应用程序，我们考虑具有微服务架构的系统，其中微服务记录事件是有条件的在系统的其他微服务中发生的事件集合的发生关键词：审计日志，并发系统，编程语言，安全性1介绍可靠的审计日志记录对于通过审计日志的事后分析提供安全计算至关重要。审计日志记录与预防性安全机制一起使用，以实现安全的深入实施。安全性的深入实施是指多层的预执行、运行时和后执行技术，以确保计算的合法性。这样的例子比比皆是，例如，实施预防措施的医疗记录系统，包括用户认证、静态/动态信息流分析以防止数据泄漏或损坏[47]，以及访问授权，例如，拒绝某些用户非法访问某些医疗数据。此外，该系统还为不同目的收集和事后分析审计日志，包括满足问责目标，例如，由健康保险可携带性和责任能力法案（HIPAA）[16，15]建立，加强访问控制[56，12]等。1电子邮件：samirmohammadian@pacific.edu2电子邮件：celkari@pacific.eduhttps://doi.org/10.1016/j.entcs.2020.08.0071571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。116S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115使用审计日志和预防机制有两个主要应用：1）审计日志的执行后分析提供了一个平台，可以根据记录的证据检测安全违规[60，5]。这类日志记录策略依赖于用户责任和威慑的概念。2)审计日志用于检测预防性安全机制中现有的漏洞并改善这些机制[7，44]。在上述两种应用中，深度安全的有效性依赖于生成的审计日志及其事后分析的正确性和有效性。审计日志的正确性和有效性反映了审计日志生成中的一些挑战。正确的审计日志必须记录有关运行时行为的事实信息，这可以通过审计策略及其运行时执行机制的验证来确保。此外，正确的审计日志必须根据审计策略的规定包含足够的信息。此外，为了提高系统在审计日志收集和分析方面的性能，必须在深度安全中强调审计日志的有效性。有效的审计日志记录需要只记录有关计算的必要信息，而不是简单地收集日志中的所有事件。这些问题在野外一直具有挑战性，例如导致无法防止数据泄露，并被Open Web Application Security Project视为十大最关键的安全风险之一[50]。为了建立审计日志的正式基础，使用信息代数理论[29]定义了审计日志的一般语义[5，6]。这一工作有助于研究在所提出的信息代数框架的基础上实施审计日志策略的机制是否在这个框架中，程序执行跟踪和审计日志都被解释为信息元素。从本质上讲，执行跟踪中的信息和审计日志中的信息之间的关系是根据已建立的信息包含的概念来制定的。如果满足这个关系，则审计日志被定义为正确的。这一提法有助于将审计要求的具体化与方案分开，这在实践中具有很大的价值。通过这种方式，可以提出算法来自动检测具有审计日志功能的代码，而不是在代码中手动内联审计日志。语义框架支持实现审计规范的一般类的算法，并建立保证这些规范通过此类算法执行的条件。上述工作依赖于所提出的审计日志生成的语义框架在实践中，这种限制将框架的应用限制在生成审计日志时涉及单个执行线程的系统中。例如，在医疗记录系统[6]的案例研究中，审计日志功能被认为是对Web服务器程序的扩展，并且日志的所有先决条件都取决于在同一程序执行线程中发生的事件以打破玻璃事件为例[32]。在危急情况下，打破玻璃是为了绕过访问控制。通过打破玻璃，系统S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115117用户增加了他们在系统中的权限，以便获得某些数据，但同时承认对他们的行为负责。打破玻璃事件是记录对特定患者信息的访问的前提条件。只要此类事件发生在单线程Web服务器的执行跟踪中，医疗记录Web服务器的仪器化就可以保证正确的审计日志记录这就消除了将身份验证和授权任务分发给系统其他并发组件的可能性。这样的限制促使我们研究并发环境中审计日志的语义，它是多线程和多进程应用程序审计目的的正确实现的基础实际上，并发和分布式系统中日志记录和监控不足的真实例子，例如，最近零售商POS系统网络中的安全事件建议的语义框架需要提供一种机制，指定审计要求的基础上并发执行的痕迹。我们的框架需要足够通用，以包含不同的审计日志生成和表示方法作为其实例。信息论模型的普遍性已经在这一领域得到了证明[6]。我们证明，这样的模型可以用于并发系统。我们使用该模型来解释审计日志，指定审计日志要求，并定义并发系统中这些要求的正确执行。类似于以前的线性流程执行工作，并发环境中日志的正确性取决于审计需求的规范，通过比较日志中包含的信息和这些规范所公布的信息我们实例化我们的一般模型与successently表达的语言，以便在并发环境中指定和执行审计要求。Horn子句逻辑是用于此目的的适当语言，这是由于将执行跟踪直接建模为事实集、用于指定审计要求的足够的表达性和可用的逻辑编程实现，例如，[46、55]。一个正式的语言模型是用来指定和建立正确的执行并发系统中的审计日志策略，根据开发的框架。为此，我们使用了π演算的一个变体[35]和未标记的归约语义。这种形式主义为开发具有正确性保证的工具提供了一个模型。该模型具有以下特点。• 并发性：为了描述多线程程序和多处理器系统，该语言模型通过消息传递支持进程间通信（IPC）的并发进程执行。• 通用性：虽然不同的进程演算是描述我们的实现模型的潜在选择，但我们使用π-演算的变体，因为它的语法和语义非常这有助于制定广泛的并行系统。• 定时：我们需要能够指定感兴趣的事件的顺序，明确审计要求。例如，在打破玻璃118S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115只要玻璃已经被打破，对特定患者信息的访问就被记录。为了实现这样的规范，我们需要应用一个在系统的所有进程之间共享的定时机制。进程并发执行的每一步都会更新这个通用时间。• 命名函数：要指定审计需求，需要一个基本的安全操作单元函数可以被认为是不同语言和系统中这些基本单位的抽象。我们的语言模型支持命名功能，在每个代理的子代理使用具有上述特征的形式主义，使我们能够根据开发的语义框架，保证正确生成审计日志的并发环境建模。在本文中，我们提出了一种仪器算法，接收并发系统作为输入，并根据审计日志要求的精确规范修改系统。我们表明，该算法是正确的（基于语义框架），因此仪表并发系统生成正确的审计日志。如前所述，通过代码插装来实施审计日志策略将策略与代码分离，为使用形式化方法研究实施机制的有效性提供了基础，并且可以自动应用于遗留代码以增强系统的可问责性。由于我们的模型是基于进程演算的，IPC是通过消息传递来处理的。为正确的审计日志记录建模替代IPC方法，例如，共享内存和/或文件，被认为是潜在的未来工作。从这项工作的结果中受益的案例研究包括在多进程和多线程客户端-服务器和对等应用程序，微服务等中部署正确的日志记录功能。虽然本文提供了抽象设置中的原型instrumentation算法，但作为未来的工作，我们的目标是在Spring Boot [53]中部署我们现有的instrumentation算法，这是一种Java微服务框架，通过面向方面的编程[2]促进代码插装。1.1文件纲要本文的其余部分组织如下。在1.2节中，我们讨论了并发系统中审计日志的示例，在1.3节中，我们讨论了威胁模型。第2节回顾了审计日志的信息代数语义第3节详细讨论了实现模型。特别是，3.1节介绍了源系统的语法和语义，这是π演算的一个变体。在第3.2节中，我们研究了一类日志规范，它们断言函数调用之间的时间关系，可能在系统的不同并发组件第3.3节研究了目标系统的语法和语义在3.4节中，我们提出了我们的插装算法，以及该算法满足的感兴趣的属性。这些性质的证明在我们随附的技术报告[3]中给出。第四节讨论了相关的工作。最后，第5节总结了S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115119授权服务授权数据库应用前端患者服务患者DBFig. 1. 医疗记录系统的授权和患者微服务。文件和未来的工作。1.2示例：基于微服务的医疗记录系统在本节中，我们将给出一个过于简单的例子，说明审计日志在并发环境中的应用。我们将在本文的后面（通过示例3.1和3.2）重新讨论这个示例，以解释我们的形式框架的示例实例。许 多 应 用 程 序 已 经 将 其 架 构 从 传 统 的 单 一 结 构 转 向 面 向 服 务 的 架 构（SOA），以提高可维护性，持续部署和测试，适应新技术，系统安全性，容错性等。SOA的一种流行部署方法是将应用程序分解为一组高度协作的流程，称为微服务。微服务必须是最小的、独立的和细粒度的。最小化限制微服务访问和操作应用程序中的某些数据类型，理想情况下每个服务都有一个数据库。微服务实例在自己的容器、虚拟机或主机中独立运行。为了实现自己的目标，微服务通过消息传递或远程过程调用（RPC）与应用程序的其他微服务进行通信。朱莉[25]是用于开发具有微服务架构的应用程序的编程语言。 它的形式语义[21，36]被定义为进程演算，灵感来自π演算。更好地简化医疗服务的需求正在推动医疗记录系统向微服务发展[49]。事实上，一项新的研究表明，基于微服务的医疗保健预计将在未来几年内经历五倍的市场价值增长[61]。在下文中，我们描述了一个基于微服务的医疗记录系统的简单示例，根据问责制要求，某些事件的审计日志是必要的。图1描述了一个具有微服务架构的医疗记录系统，其中包括授权和患者服务（以及其他服务）。应用程序前端包括API网关，其多路复用用户请求（来自不同客户端，例如，web、移动应用等）一些微服务。患者微服务管理有关患者的信息，例如，他们的病史。 授权微服务处理授权访问系统数据的不同操作，包括例如，打破玻璃。120S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115如前所述，打破玻璃，用户同意遵守责任规定。遵循责任规则的常见解决方案是在运行时生成审计日志的跟踪。一个这样的审计日志记录要求可以如下：这个例子展示了我们在本文中追求的核心思想• 采用并发系统，其中每个组件独立运行并与其他组件协作，例如，具有包括上述微服务的不同微服务的医疗记录系统。• 审计日志记录要求需要在并发组件中记录某些事件，只要一组其他事件先前已经在潜在的其他并发组件中发生，例如，如果玻璃已经在授权微服务中破碎，则在患者微服务中记录读取病史的事件• 我们研究了一种算法的方法，以建立正确的审计日志的当前环境，根据已经建立的审计日志的要求。例如，在我们的医疗记录系统示例中，我们期望审计日志记录的正确性意味着只记录打破玻璃的用户的读取尝试。这样可以避免遗漏任何日志记录事件以及记录不必要的事件。我们通过检测授权和患者微服务来实现这一点打破玻璃读病人的病史1.3威胁模型我们假设受到插装的并发系统首先不支持审计日志记录，或者是由于审计日志生成不足或过于热心而导致的。然而，我们假设根据我们的实现模型部署的并发系统通过了静态和动态检查，例如，语法检查、类型检查、编译、解释等。我们信任编译器/解释器，以及执行系统的运行时环境。此外，我们信任我们的插装算法的实现我们也信任声明审计日志记录要求的日志记录规范的完整性。最后，我们信任的编译/解释过程的仪表并发系统，部署基于我们的实现模型，以及系统并发组件之间传输的消息和生成的审计日志的安全性被认为超出了范围。这些假设帮助我们有目的地关注日志记录的本质，即，日志是否首先正确生成，并且独立于外部问题，包括底层执行和通信系统的可靠性、延迟等，这些在相关工作中进行了探讨（第4节）。S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）11512132审计日志为了提供一个独立的正式介绍，在本节中，我们回顾审计日志的信息代数语义和使用一阶逻辑的语义框架的实例化，这最初是由Amir- Mohammadian等人提出的。我们对模型进行了一些小的修改，以更好地适应并发系统固有的并发性和不确定性运行时行为。2.1信息-代数语义框架为了说明审计日志在运行时是如何生成的，我们需要抽象系统状态及其在计算过程中的演变系统配置κ抽象了系统在执行过程中给定点的状态。设K表示系统配置的集合我们在配置之间建立了一个二元归约关系，即，（−→）K × K，表示计算步骤，用于标准的固定形式。 系统迹τ是系统配置的潜在无限序列，即，τ=κ0κ1···，其中κi是序列中的第i个配置，且κi−→κi+1。我们用T表示所有迹的集合，并将prefix（τ）定义为τ的所有前缀的集合。信息代数用于定义审计日志的正确性概念。在第2.2节中，我们实例化了这个抽象代数结构来建模一类特定的审计日志需求。我们在下面定义一个信息代数。定义2.1（信息代数）信息代数（Φ，φ）是一个双排序代数，由信息元素的阿贝尔半群Φ和查询域的格φ组成。 假定两个基本算子在这个代数中：一个组合算子，（）：Φ× Φ → Φ，和一个聚焦算子，（）：Φ × Φ → Φ。一个信息代数（Φ，φ）满足一组与组合和聚焦算子有关的性质。[4]我们让X、Y、Z、···在Φ的所有元素上取值，让E在 Φ 的 所 有 元 素 上 取值。X、Y∈Φ是可以组合以形成更包含的信息元素X∈Y的信息元素。E∈E是具有一定粒度级别的查询域，聚焦算子使用该查询域从信息元素X，由X∈E表示。例如，关系代数是信息代数的一个实例，其中关系实例化信息元素，属性集实例化查询域，两个关系的自然连接定义组合运算符，关系在属性集上的投影定义聚焦运算符[29]。信息元素的组合导致信息元素之间的偏序关系（直观地说，X[3]贯穿全文的一个符号约定是，当指定了它们的签名时，用括号将整型运算符和关系包装起来。[4]为了简洁起见，我们在这里避免详细讨论这些性质读者可参考[29]以了解完整的公式。122S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115作为审计日志语义的一部分，我们将执行跟踪视为信息元素，即，执行轨迹的信息内容。为此，我们将[·τ：T →Φ]作为一个映射，其中[ττ]直观地指迹τ的信息内容。我们还施加条件，即[·]是单射和单调递增的，即， 如果τ J∈prefix（τ），则[τ J<$“[τ<$. 这确保了随着执行跟踪长度的增长，它包含更多的信息。在以下定义中，我们以抽象形式定义了审计日志记录要求。我们称这种抽象为日志规范。这个定义足够抽象，可以包含不同的执行模型，以及不同的信息表示。在2.2和3.2节中，我们用一个更具体的结构来实例化这个定义，它指导我们如何实现审计日志需求。定义2.2（日志规范）日志规范LS被定义为从系统轨迹到信息元素的映射，即，LS：T → Φ。直觉上，LS（τ）声明了如果系统遵循执行轨迹τ，则必须记录哪些信息。请注意，即使[*]和LS具有相同的签名，即，从轨迹映射到信息元素，它们在概念上是不同的。[τ是包含在τ中的全部信息，而LS（τ）是假设记录在日志中的信息，如果系统遵循执行轨迹τ。我们用L表示审计日志，它表示在运行时收集的一组数据。让L表示审计日志集。为了判断审计日志的正确性，需要将审计日志的信息内容与生成该审计日志的跟踪的信息内容进行比较。 为此，我们定义了一个映射，它返回审计日志的信息内容。我们滥用了这个符号，把[·L：L →Φ]看作这样的映射.因此，[L]是指审计日志L的信息内容。我们假设审计日志上的[·k]是单射的且单调递增，即，如果L<$LJ，则[L<$“[ L J <$”。因此，审核日志的包容性越强，它包含的信息就越多。正确审计日志的概念可以根据执行跟踪和日志规范来定义。为此，将审计日志的信息内容与日志规范要求记录的信息进行比较在日志中，给出了执行跟踪。下面的定义抓住了这种关系。定义2.3（审计日志的正确性）审计日志L对于日志规范LS和系统跟踪τ i都是正确的，[L“LS（τ）和LS（τ）“[ L hold。前者是指审计日志中信息的必要性，后者是指审计日志中信息的充足性在运行时生成审计日志的系统包括存储的日志，其配置。设映射logof：K →L表示给定的系统配置，即，logof（κ）是配置κ中所有记录的审计日志的集合。很自然地，我们会假设配置中的剩余日志会随着执行的进行而变大。然后使用logof定义跟踪的剩余对数。S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115123定义2.4（系统道的剩余对数）有限个系统道τ的剩余对数为L，记为τ~L，iτ = κ0κ1···κn，logof（κn）=L。注意，如果τ~L，则L对于给定的LS和迹τ不一定正确。如果跟踪的剩余日志在整个执行过程中都是正确的，则该跟踪被称为理想检测的。对于任何跟踪τJ和审计日志L，系统跟踪τ理想地被仪表化用于日志规范LSi，如果τJ∈prefix（τ）且τJ~L，则L对于τJ和LS是正确的。事实上，审计日志是执行跟踪上的可强制执行的安全属性[6]。给定一个日志规范，理想的仪表跟踪会产生一个安全属性[43]，因此可以通过内联引用监视器[18]和编辑自动机[4]实现。让我们成为一个具有操作语义的并发系统 s τ i s可以产生迹τ J，无论是确定性的还是非确定性的，并且τ ∈ prefix（τ J）。我们滥用了这个符号，用κ τ来表示构形κ的同一个概念。我们遵循程序插装技术，以便在系统上强制执行日志规范。插装算法接收并发系统作为输入以及日志规范，并使用审计日志功能插装系统，以便插装系统生成所需的“适当”日志。插装算法是根据LS插装s的部分函数I：（s，LS）›→ sJ，旨在生成适合LS的审计日志。我们称之为源系统和指令系统，即， I（s，LS）=SJ，目标系统。 源跟踪和目标跟踪分别指源系统和目标系统的跟踪。很自然地，可以预期插装算法不会彻底修改原始系统除了与审核日志记录相关的操作之外，目标系统的行为必须我们将插装算法的这个属性称为语义保留，并在下面对其进行定义。这个定义足够抽象，可以包含不同的源系统和目标系统（具有不同的运行时语义）以及插装技术。这种抽象依赖于一种二元关系：对应关系（correspondence relation），它将源轨迹和目标轨迹联系起来。基于源系统和目标系统的不同实现以及插装算法，可以相应地定义对应关系。定义2.5（通过插装算法的语义保持插装算法I是用于所有系统s和日志记录特性LS的语义保持插装算法，其中定义了I（s，LS），以下条件成立：1）F或任何traceτ，如果s∈τ，则re存在某个traceτJ，使得I（s，LS）∈τJ，并且τ：ττJ。2）F或任意traceτ，如果I（s，LS）∈τ，则re存在某个traceτJ，使得那是<$τ J，τ J：<$τ。插装算法的另一个相关属性是确保它是无死锁的，这意味着插装系统不会引入被卡住的新状态。定义无死锁的独立概念的一种方法是考虑双相似的源和目标跟踪。实际上，必须引入额外的形式化结构来将目标跟踪转换为源跟踪。我们124S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115我然而，无死锁的定义在很大程度上依赖于语义保持的概念，并且不是定义插装正确性的必要组成部分（定义2.7）。 设源系统s生成迹τ，且I（s，LS）生成迹τJ，则τ：ττJ。然后，如果s可以在τ之后继续执行（至少对于一个额外的步骤），而（s，LS）不能在τ j之后继续执行，则我们调用I（S，LS）。定义2.6（插装算法的无死锁性）插装算法I对于任何源系统s都是无死锁的，记录了L S中的specati，tracesτ和τJ，以及约束κ，如果s <$τ，I（s，LS）<$τJ，τ：<$τJ，和s <$τκ，则re存在某种约束κJ，使得I（s，LS）<$τJκJ。除了这些属性之外，检测算法的另一个重要特性是由检测系统生成的审计日志的质量。信息代数语义框架提供了一个平台，用于定义用于审计日志记录目的的正确指令算法。 设s为目标系统，τ为源迹。 τ乘s的模拟对数是simlogs（s，τ）的集合，定义为simlogs（s，τ）={L|我是j. j.s<$τ J<$τ：<$τ j<$τ J~ L}。 使用这个集合，我们可以直接定义插装算法的正确性。直观地说，如果检测系统生成的审计日志在日志规范和源跟踪方面都是正确的，那么检测算法I就是正确的。 这必须适用于任何源系统、任何日志规范以及由检测系统生成的任何可能的日志。定义2.7（插装算法的正确性）插装算法I对于所有源系统s、迹线τ和L∈S，s∈τ是正确的，意味着对于任何L∈S（I（s，LS）， τ），L对于LS和τ是正确的。2.2日志规范的实例化在定义2.2中，日志规范被抽象地定义为从系统跟踪到信息元素的映射对于更具体的设置，需要使用适当的结构实例化此定义，以便于部署审计日志。本质上，我们需要实例化信息代数（定义2.1）。我们对审计日志需求的逻辑规范感兴趣，因为它易于使用、表达能力强、语义易于理解，以及用于一阶逻辑（FOL）子集的自适应逻辑编程引擎，例如，Horn子句逻辑。为此，在本节中，我们用FOL实例化信息代数，FOL具有足够的表达能力来指定计算事件以及它们之间的实际上，出于此目的，也可以考虑逻辑的其他变体。为了实例化信息代数，需要指定信息元素集合Φ的内容和查询域的格，以及组合和聚焦运算符的定义定义2.8、2.9和2.10完成这些实例化。定义2.8实例化了一组基于FOL-based的信息元素。一个在-S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115125在我们的实例化的形成元素是一个封闭的FOL公式集，在证明理论演绎系统。定义2.8（FOL公式的闭集的集合）设Γ range在FOL公式上，Γ range在FOL公式的集合上。它表示由FOL的一个可靠的、完备的自然演绎证明理论导出的一个 判 断 。 我 们 将 闭 包 运 算 Closure 定 义 为 Closure （ Γ ） = {\displaystyle\close（Γ）}。|我知道了。 然后，闭集的集合F O L 公式的定义为Φ FOL={Γ| r=闭包（r）}。定义2.9实例化了基于FOL-based信息代数的查询域的格。查询域是FOL的一个子集，由某些谓词符号定义。定义2.9（FOL子语言的格）设Preds是所有假定谓词符号及其对象的集合。如果S是Preds，那么我们将子语言FOL（S）表示为S中谓词符号上的格式良好的FOL公式的集合。所有这些子语言的集合<$FOL={FOL（S）|SPreds}是由集合包含关系诱导的格。最后，定义2.10实例化了基于FOL-based信息代数的组合和聚焦运算符。组合是两组公式的并集的闭包。聚焦是信息元素和查询域的交集的闭合。定义2.10（在（ΦFOL， ΦFOL）中组合和聚焦）设（1）：ΦFOL×ΦFOL→ ΦFOL被定义为 Γ ΓJ =闭包（Γ ΓJ），并且（1）：Φ FOL× φ FOL→ Φ FOL定义为：Γ φFOL（S）=闭包（Γ φFOL（S））.（ΦFOL， ΦFOL）是一个信息代数，给出定义2.8，2.9，和两点十分5为了使用（Φ FOL，FOL）作为审计日志的框架，我们还需要实例化2.1节中介绍的映射[·]，以将执行跟踪和审计日志解释为信息元素。定义2.11（将跟踪和审计日志映射到（Φ FOL，Φ FOL）中的信息元素）设toFOL（·）：（T ΦFOL）→FOL（Preds）是单射单调递增函数。然后，我们实例化[·= Closure（toFOL（·）），以便解释这两个轨迹和记录作为（Φ FOL，Φ FOL）中的信息元素。现在我们可以在信息代数（ΦFOL， ΦFOL）中实例化日志规范LS。为此，在FOL中假定给出了一组审计日志规则和定义。设r为这个集合。 此外，假设一组谓词符号反映谓词，其派生需要在运行时记录。这个集合用S表示。在这种情况下，测井规范接收道τ，将τ的信息内容与τ的闭包相结合，然后聚焦在S中指定的谓词上。直觉上，给定Γ和S，一个日志规范将一个迹τ映射到所有谓词的集合，这些谓词的符号在S中，并且在给定Γ中的规则和τ中的事件时是可导出的。[5]详细的证明可参考文献[4]，它依赖于FOL的自然演绎系统的性质。126S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115定义2.12（（Φ FOL，Φ FOL）中的日志规范）给定一组FOL公式Γ和一个谓词符号子集S<$Preds，日志规范规范（Γ，S）：T → Φ FOL定义为spec（Γ，S）= τ<$→（[ τ <$闭包（Γ））<$FOL（S）。3并发系统在本节中，我们提出了一个在并发系统中正确审计日志记录的实现模型。为此，我们使用π-演算的一个变体来指定并发系统，并提出了一个插装算法，该算法根据给定的日志规范对系统进行改造。然后，我们指定并证明感兴趣的属性，包括插装算法的正确性（定义2.7）。在第3.1节中，介绍了源系统模型的语法和语义。第3.2节提出了一类日志规范，可以指定并发系统中计算事件之间的时间关系。第3.3节描述了使用审计日志功能增强的系统的语法和语义。最后，在3.4节中，我们讨论了插装算法及其满足的性质。3.1源系统模型我们考虑一个核心的π演算作为我们的源并发系统模型，表示为Π。 π演算的一个主要区别特征是使用相同类别的名称为链接和可转移对象建模移动流程，以及范围挤压。然而，在我们的实现模型中没有使用移动性。因此，其他精突结石，例如，CSP [23]和CCS[34]也可以考虑用于此目的。我们采用π演算，因为它简洁的语法和简单的语义，提供了一个干净的和successently抽象的规范所需的系统并发组件之间的相互作用。源系统的语法和语义定义如下。它基于[38]中给出的微积分的表示，为了简单和简洁，它通过放弃沉默前缀，无保护求和和标记归约系统而偏离标准π3.1.1语法设N是无限可数的名称集合，a，b，c，···和x，y，z，····在它们上面。PrefixesPrefixesα定义为sα：：=a（x）|a'x.Prfixa（x）是输入前缀，用于接收链接a上带有占位符x的名称。 Prfixa<$x是输出前缀，用于在链接a上输出名称x。设A，B，C，D为所有代理名称的范围，A为这些名称的有限集合。过程P定义为：P：：=0 |α.P|（P|（P）|（νx）P|C（y1，···，yn）. 0表示nil进程。 α.P提供了流程中的一系列操作;第一个输入/输出前缀α采用S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115127.Σplace，然后P执行。P|P在系统中提供并行性。（νx）P在P内限制（约束）名字x。C（y1，···，yn）指的是使用参数y1，···，yn调用代理C。设P，Q，R在过程上值域.自由和绑定名称进程中的名称限制和输入前缀绑定名称。我们用fn（P）表示进程P中的自由名集合。绑定名称的α-转换以标准方式定义一 系 列 名称用 字 母 表 示 ， 即 ， a1 ， ·· · ， al 代表 某个 l 。 过 程（ νa1 ）（νa2）··（νal）P中 的 一 系 列 名 称 限 制 由 （νa1a2·· ·al ）P表 示 ， 或 在h或t（νa）P中表示. 如果输入名称在以下过程中不空闲，则我们跳过指定输入名称，即，a.P指a（x）.P，其中x∈f n（P）。P是指在链路a上输出可以省略的值，例如， 由于缺乏相关性的讨论。代码库Agent定义的形式为A（x1，···，xn）P。 让我们假设存在一个由这种形式的智能体定义组成的通用代码库CU此代码库用于定义顶级代理。顶层代理对应于系统的并发组件。顶层代理应该并行执行，偶尔相互通信以完成自己的任务，并聚集在并发系统中。设AU是顶级代理名称的集合，使得AU=A。 在整个论文中，我们让m是AU的大小，包括的A1，···，Am. CU被定义为从顶级代理名称到其定义的函数，即，CU：AU→D。此外，我们假设每个顶级代理都存在一个本地代码库，对于顶级代理A，用CL（A）表示。局部代码库由形式为BA（x1，···，xn）P的子代理（子进程）定义组成，其中B是子代理标识符，A是在B的定义中注释的顶级代理标识符。我们将子代理视为顶级流程的内部模块或功能。顶级代理标识符的注释用于此目的，即，BA指定B是顶级代理A的模块。子代理名称的集合用AL表示，定义为A− AU。CL被定义为具有签名CL的函数：AU→ AL→ D。请注意，任何进程和子进程的定义都可以是递归的，例如，如果CU（A）=[A（x1，···，xn）P]，则A（y1，···，yn）可能出现在P中.在下文中，我们使用A和B分别包括顶级代理标识符和子代理标识符。我们使用C来覆盖顶级代理A和子代理BA。 在本文的其余部分，我们简单地用“代理人”来指代顶级代理人。我们假设在任何（子）过程定义C（x1，···，xn）P中，我们有fn（P）<${x1，···，xn}。 这确保了（子）进程是关闭的。初始系统设AU={A1，·· ·，Am}. 我们设置了一个链接序列，用于连接系统中的这些代理。初始并发系统s定义为：s：：=Ps，CU，CL，（1）其中Ps=（νc）（A1（x<$1））|A2（x2）|···|Am（x<$m）），假设f n（Ps）=n，即，ixic.我们将系统配置定义为κ：：=P，其中P是128S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115与整个系统相关的过程。初始构型则定义为κ0=Ps。置换是一个函数σ：N → N。符号{y/x}用于表示将x映射到y的替换，否则充当恒等函数。用{y_n/x_n}表示一个代换中的多个显式映射，其中x_n和y_n的长度相等。 P σ是指根据σ替换P中的自由名。这与重命名P中的绑定名称有关，以避免名称冲突。3.1.2语义在下文中，我们定义了评估上下文和过程之间的结构一致性。这些定义以简洁的方式促进了未标记操作语义的具体化。评估上下文上下文是一个有漏洞的过程。评估上下文E是其孔不在输入/输出前缀下的上下文，即， E：：=[客户端]|（E）|（P）|（P| E）的|（νa）E.两个进程P和Q在通用代码库CU下是结构上全等的，根据以下规则用CUDPQ(i) 结构全等是一种等价关系。(ii) 结构同余通过应用E闭合，即， CUDP[1][2][3][4][5][6][7(iii) 如果P和Q是α-可转换的，则CUDP<$Q。(iv) 过程集是阿贝尔半群，|运算符和单位元素0，即，对于任何CU，P，Q和R，我们有CUDP|0美元，CUDP|QQ|P和CUDP|（Q|R）（P |Q）|R.(v) 如果CU（A）=[A（x<$）P]，则CUDA（y<$）<$P{y<$/x<$}.(vi) C UD（νa）0 0。(vii) 若a∈/fn（P），则CUD（νa）（P|Q）可持续发展|（νa）Q.(viii) C UD（νa）（νb）P（νb）（νa）P.如果从上下文中可以清楚地看出，我们可以在结构全等的具体化中省略CU我们在图2中定义了未标记的归约系统，使用判断CU，CLDκ−→κJ。我们可以在约简步骤的指定中省略CU和CLκ−→κJ。请注意，根据结构一致性规则，代理调用在结构上与其定义（第五部分）一致，因此根据规则STRUCT被视为执行的这是由于我们建模中的一些技术性问题：子代理的调用可能是记录先决条件和/或记录事件（在3.2节中介绍），因此需要特殊的语义处理。S. Amir-Mohammadian角Kari/Electronic Notes in Theoretical Computer Science 351（2020）115129STRUCTCUDPP′CU， CLDP′−→Q′CUDQQ′CU， CLDP−→Q上下文CU，CLDP−→QCU， CLDE[P]−→E[Q]呼叫C，CDBA（y）−→P{y/x}CL（A）（B）=[B（x）P]一ULCommCU，CLDa（x）.P|a<$b.Q−→P{b/x}|Q图二、 未标记的约简语义。调用时的事件（稍后在第3.3节和第3.4节中讨论），例如， 决定记录是否必须存储在日志中对于（潜在无限）系统迹τ=κ0κ1···，我们使用符号CU，CL<$τ来指定迹τ在通用和局部码基CU和CL下的生成，并且根据上述未标记的约简系统，即，CU，CLDκi−→κi+1，对所有i∈ {0， 1，···}。对于一个系统迹τ=κ0κ1···，系统s生成τ，记为sτis定义为（1），κ0定义为Ps，且对于所有i∈ {0， 1，···}，CU，CLDκi−→κi+1。为了在逻辑上指定一个跟踪，我们需要根据定义2.11实例化toFOL（·）。我 们 考 虑 以 下 谓 词 来 逻 辑 地 指 定 跟 踪 ： Comm/3 、 Call/4 、 Context/2 、UniversalCB/3和LocalCB/4。6令CU，CL<$τ，τ=κ0···κκJ···。此外，让t表示定时计数器。我们定义了一个函数，它在逻辑上指定了轨迹中的配置。为此，让helper函数toFOL（κ，t）返回κ在时间的t.从本质上讲，toFOL（κ，t）指定了在时间t时κ内的求值上下文和redex，定义如下：(i) 到FOL（k，t）={Comm（t，a（x）. P，a<$b.Q），Co ntext（t，E）}，7ifκE[a（x）.P|a<$b.Q]和κjE[P{b/x}|Q]。