完善的应用软件安全监控
Sound and Complete Runtime Security Monitor for Application Software
摘要：
通过监控来确保运行时应用软件安全性的传统方法要么产生（高比率）假警报（例如入侵检测系统），要么限制应用程序性能（例如运行时验证）。我们提出了一个运行时安全监视器，检测已知和未知的网络攻击，通过检查应用程序的运行时行为是一致的应用程序规范中建模的预期行为。这是至关重要的，因为即使实现与其规范一致，应用程序仍然可能由于支持基础设施（例如语言运行时系统、库和操作系统）中的缺陷而易受攻击。这个运行时安全监视器是健全和完整的，消除了错误警报，以及高效，所以它不会限制运行时应用程序的性能，所以它支持实时系统。安全监视器将可以用不同语言表达的应用规范和应用实现作为输入。基于一元二阶逻辑和代数数据结构上的事件演算对应用软件的规约语言进行了形式化。这种语言允许我们在任何期望的（和实际的）抽象级别以及高度的模块化来表达应用程序的行为。安全监视器通过系统地比较运行时的应用程序执行和规范行为来检测每一次攻击，即使它们在两个不同的抽象级别上操作。我们定义了规约语言的指称语义，并证明了监控器是健全和完整的。此外，由于在适当的抽象级别上的模块化应用规范，监视器是高效的。
英文摘要：
Conventional approaches for ensuring the security of application software at run-time, through monitoring, either produce (high rates of) false alarms (e.g. intrusion detection systems) or limit application performance (e.g. run-time verification). We present a runtime security monitor that detects both known and unknown cyber attacks by checking that the run-time behavior of the application is consistent with the expected behavior modeled in application specification. This is crucial because, even if the implementation is consistent with its specification, the application may still be vulnerable due to flaws in the supporting infrastructure (e.g. the language runtime system, libraries and operating system). This runtime security monitor is sound and complete, eliminating false alarms, as well as efficient, so that it does not limit runtime application performance and so that it supports real-time systems. The security monitor takes as input the application specification and the application implementation, which may be expressed in different languages. The specification language of the application software is formalized based on monadic second order logic and event calculus interpreted over algebraic data structures. This language allows us to express behavior of an application at any desired (and practical) level of abstraction as well as with high degree of modularity. The security monitor detects every attack by systematically comparing the application execution and specification behaviors at runtime, even though they operate at two different levels of abstraction. We define the denotational semantics of the specification language and prove that the monitor is sound and complete. Furthermore, the monitor is efficient because of the modular application specification at appropriate level(s) of abstraction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
