OACAL：寻找模块一致的规范，以保护系统免受削弱的用户义务的影响
OACAL: Finding Module-consistent Specifications to Secure Systems from Weakened User Obligations
摘要：
通过UI与系统交互的用户通常有义务按照预定顺序执行其操作，以成功实现某些功能目标。然而，这些义务往往没有严格遵守的用户，这可能会导致违反安全属性，特别是在安全关键系统。为了提高系统的安全性和对意外用户行为的感知，可以通过改变系统规范中的操作顺序来重新设计系统，使其更健壮。与此同时，我们预计在修改后功能将保持一致。在本文中，我们提出了一个有效的算法来自动产生规范修订解决攻击的情况下所造成的削弱用户的义务。通过我们的算法，所有的修订将被生成，以保持完整的功能，使用一种新的重组方法。然后，可以满足安全要求的合格的修订将有效地发现模型检验和机器学习技术相结合的混合方法。我们评估我们的算法通过比较其性能与国家的最先进的方法，其覆盖范围和搜索速度的理想的修订。
英文摘要：
Users interacting with a system through UI are typically obliged to perform their actions in a pre-determined order, to successfully achieve certain functional goals. However, such obligations are often not followed strictly by users, which may lead to the violation to security properties, especially in security-critical systems. To improve the security with the awareness of unexpected user behaviors, a system can be redesigned to a more robust one by changing the order of actions in its specification. Meanwhile, we anticipate that the functionalities would remain consistent following the modifications. In this paper, we propose an efficient algorithm to automatically produce specification revisions tackling the attack scenarios caused by weakened user obligations. By our algorithm, all the revisions would be generated to maintain the integrity of the functionalities using a novel recomposition approach. Then, the eligible revisions that can satisfy the security requirements would be efficiently spotted by a hybrid approach combining model checking and machine learning techniques. We evaluate our algorithm by comparing its performance with a state-of-the-art approach regarding their coverage and searching speed of the desirable revisions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
