OACAL: Finding Module-consistent Specifications to Secure Systems from Weakened User Obligations

TL;DR

This paper presents an algorithm that automatically revises system specifications to enhance security against weakened user obligations, ensuring functionality remains consistent while preventing security violations.

Contribution

It introduces a novel recomposition-based algorithm combined with model checking and machine learning to efficiently generate and identify secure specification revisions.

Findings

The algorithm outperforms existing approaches in coverage and speed.

It effectively maintains system functionality while improving security.

Evaluation shows significant efficiency gains in revision generation.

Abstract

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.