Biblio

Reactive systems respond to requests from an environment with appropriate timing. Because reactive systems are used widely in infrastructure, it is necessary that they are developed without flaws. Automatic synthesis of reactive systems from particular specifications is an ideal technique for ensuring development without flaws. Several tools for synthesis have been proposed, e.g., Lily, AcaciaPlus and Unbeast. Among them, AcaciaPlus can synthesize systems compositionally, and enables synthesis from large-scale specifications that could not previously be treated. However, the modularization of specifications depends largely on the computation time required for synthesis; this is not a trivial problem. In this paper, we discuss the modularization of specifications to enable efficient synthesis of reactive systems.

Firewall policies are notorious for having misconfiguration errors which can defeat its intended purpose of protecting hosts in the network from malicious users. We believe this is because today's firewall policies are mostly monolithic. Inspired by ideas from modular programming and code refactoring, in this work we introduce three kinds of modules: primary, auxiliary, and template, which facilitate the refactoring of a firewall policy into smaller, reusable, comprehensible, and more manageable components. We present algorithms for generating each of the three modules for a given legacy firewall policy. We also develop ModFP, an automated tool for converting legacy firewall policies represented in access control list to their modularized format. With the help of ModFP, when examining several real-world policies with sizes ranging from dozens to hundreds of rules, we were able to identify subtle errors.

Firewall policies are notorious for having misconfiguration errors which can defeat its intended purpose of protecting hosts in the network from malicious users. We believe this is because today's firewall policies are mostly monolithic. Inspired by ideas from modular programming and code refactoring, in this work we introduce three kinds of modules: primary, auxiliary, and template, which facilitate the refactoring of a firewall policy into smaller, reusable, comprehensible, and more manageable components. We present algorithms for generating each of the three modules for a given legacy firewall policy. We also develop ModFP, an automated tool for converting legacy firewall policies represented in access control list to their modularized format. With the help of ModFP, when examining several real-world policies with sizes ranging from dozens to hundreds of rules, we were able to identify subtle errors.