FWS: Analyzing, maintaining and transcompiling firewalls

Firewalls are essential for managing and protecting computer networks. They permit specifying which packets are allowed to enter a network, and also how these packets are modified by IP address translation and port redirection. Configuring a firewall is notoriously hard, and one of the reasons is that it requires using low level, hard to interpret, configuration languages. Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another. To address these issues we introduce a pipeline that assists system administrators in checking if: (i) the intended security policy is actually implemented by a configuration; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior; (iv) there are useless or redundant rules; additionally, an administrator can (v) transcompile a configuration into an equivalent one in a different language; and (vi) maintain a configuration using a generic, declarative language that can be compiled into different target languages. The pipeline is based on IFCL, an intermediate firewall language equipped with a formal semantics, and it is implemented in an open source tool called FWS. In particular, the first stage decompiles real firewall configurations for iptables, ipfw, pf and (a subset of) Cisco IOS into IFCL. The second one transforms an IFCL configuration into a logical predicate and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior. System administrators can use FWS to analyze the firewall by posing SQL-like queries, and update the configuration to meet the desired security requirements. Finally, the last stage allows for maintaining a configuration by acting directly on its abstract specification and then compiling it to the chosen target language. Tests on real firewall configurations show that FWS can be fruitfully used in real-world scenarios.

Mediational Fields and Dynamic Situated Senses

"The purpose of this paper is to introduce the notions of mediational fields and dynamic situated senses as a way to identify the structure of experiences, thoughts and their relations. To reach this purpose I draw some lessons from the debate between Dreyfus and McDowell about the structure of experience, from Cussins’s conception of mediational contents, and from Evans’s account of singular senses. I notice firstly that McDowell’s answer to Dreyfus consists in developing a practical and demonstrative notion of the products of our conceptual capacities. A conception that entails that human experience is not entirely characterised in terms of an abstract specification of truth-conditions. McDowell and Cussins endorse Evans’s conception of singular senses. A specification that takes into account the dynamic and situated abilities involved in making reference. Whereas the first argues in favour of a conceptual conception of experience, the second one argues in favour of a nonconceptual conception. I introduce the notions of mediational fields and dynamic situated senses to argue that both converge in conceiving the contents of experience as mediational and not reducible to an abstract specification of truth-conditions. My proposal is to define a bidimensional space orthogonal to the conceptual/ nonconceptual, experience/thought, know-how/know-that dichotomies. Cognitive contents are ways to disclose the world both as mediational fields and as referential structures. The degree in which those elements are presented determine different varieties of cognition. I use the previous notions to develop the sketch of an account of singular, objective and contextual ways of cognition, and to argue that it is better to begin an enquiry about cognition with notions that do not presuppose a distinction between practical and intellectual capacities. Keywords: Mediational Contents, Nonconceptual contents, Dynamic Thoughts, Singular Reference, Context-Sensitivity."

Formalizing Timed BPEL by D-LOTOS

Different standards and languages are proposed in the literature to model the composition of Web services. Unfortunately these languages are essentially syntactic and thus contain much ambiguity and inconsistency. In addition, the formal verification of the proposed languages is impossible. In this paper, the authors propose a transformation approach allowing the formal representation, analysis and refinement of Web services compositions. Both timed constraints and the durations of interactions between these services are taken into account. The authors present a mapping from Web services described in the BPEL language to an abstract specification written in the real-time language D-LOTOS which is based on true-concurrency semantics.

Pointwise extensions of GSOS-defined operations

Final coalgebras capture system behaviours such as streams, infinite trees and processes. Algebraic operations on a final coalgebra can be defined by distributive laws (of a syntax functor Σ over a behaviour functor F). Such distributive laws correspond to abstract specification formats. One such format is a generalisation of the GSOS rules known from structural operational semantics of processes. We show that given an abstract GSOS specification ρ that defines operations σ on a final F-coalgebra, we can systematically construct a GSOS specification ρ that defines the pointwise extension σ of σ on a final FA-coalgebra. The construction relies on the addition of a family of auxiliary ‘buffer’ operations to the syntax. These buffer operations depend only on A, so the construction is uniform for all σ and F.