OACAL: Finding Module-Consistent Solutions to Weaken User Obligations

Users interacting with a UI-embedded machine or system 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. In order 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 with attack scenarios caused by the weakened user obligations. By our algorithm, all the revisions maintain the integrity of the functionalities as the original specification, which are generated using a novel recomposition approach. Then, the qualified 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.