OACAL: Finding Module-consistent Specifications to Secure Systems from Weakened User Obligations
This addresses security vulnerabilities in systems with user interfaces, particularly in security-critical domains, by providing an automated method to redesign specifications, though it appears incremental as it builds on existing model checking and machine learning techniques.
The paper tackles the problem of securing systems from weakened user obligations by automatically generating specification revisions that maintain functional consistency while satisfying security requirements, achieving improved coverage and search speed compared to a state-of-the-art approach.
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.