Bounded Serial Compositional Runtime Enforcement

doi:10.5381/jot.2026.25.1.a11

Bounded Serial Compositional Runtime Enforcement

2026-01-01

0

PRE

AI

DOI：10.5381/jot.2026.25.1.a11

原文链接

原文求助

摘要

En 中文

运行时强制是一种用于确保系统按照一组形式属性进行操作的监控技术。它采用一个强制器，将不可信的事件序列转换为一个满足指定属性的序列。在属性违反的情况下，我们允许强制器暂时延迟输入事件（即将其存储在内存中，直到属性能够被满足），或者如果属性永远无法被满足，则抑制这些事件。本文探讨了对多个（无时间限制）属性进行强制执行的问题，这些属性被建模为有限自动机，其中强制器被串联组合，以促进模块化，即，我们不是为所有属性合成一个单一的强制器，而是生成个体强制器并串联组合它们。此外，为了处理实际约束，本文考虑每个强制器在有限（有界）内存下运行。我们探讨了在内存约束的复合设置下，是否可以强制执行正则属性及其子类，特别是安全属性（不会发生坏事）和共安全属性（最终会发生好事）。我们通过保留诸如正确性、透明性等关键标准来定义可强制执行性。对于并非固有地可以串联强制执行的属性，我们识别其自动机上的特定条件，这些条件的满足允许某些属性组成为可以串联强制执行的。为了形式化并支持这些想法，我们提出了有界串联复合运行时强制框架。我们提供了一个原型实现，并评估了所提出的串联强制器的性能，以证明其实际可行性。

Keyword:

Formal verification

Runtime enforcement

Bounded-memory

Serial composition

Regular property

Safety and co-safety property

Automata

Bounded Serial Compositional Runtime Enforcement

摘要

期刊

机构

引用论文