Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework

C. Dubois, P. Masci, D. Méry (Eds.): F-IDE 2016 EPTCS 240, 2017, pp. 38–52, doi:10.4204/EPTCS.240.3 © G. Le Guernic, B. Combemale & J.A. Galindo This work is licensed under the Creative Commons Attribution License. Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework Gurvan LEGUERNIC DGA Maîtrise de l’Information 35998 Rennes Cedex 9, France Benoit COMBEMALE José A. GALINDO INRIA RENNES – BRETAGNE ATLANTIQUE Campus universitaire de Beaulieu 35042 Rennes Cedex, France Many project-specific languages, including in particular filtering languages, are defined using nonformal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach. 1 Introduction Packet filtering (accepting, rejecting, modifying or generating packets, i.e. strings of bits, belonging to a sequence) is a recurring problematic in the domain of information systems security. Such filters can serve, among other uses, to reduce the attack surface by limiting the capacities of a communication link to the legitimate needs of the system it belongs to. This type of filtering can be applied to network links (which is the most common use), product interfaces, or even on the communication buses of a product. If the filtering policy needs to be adapted during the deployment or operational phases of the system or product, it is often required to design a specific language L(syntax and semantics) to express new filtering policies during the lifetime of the system or product. This language is the basis of the filters that are applied to the system or product. Hence, it plays an important role in the security of this system or product. It is therefore important to have strong guarantees regarding the expressivity, precision, and correctness of the language L(meaning that everything that need to be expressed can, and that everything that can be expressed has the most obvious semantics). Those guarantees can be partly provided by a formal design (and development) process. Among diverse duties, the DGA (Direction Générale de l’Armement, a french procurement agency) is involved in the supervision of the design and development of filtering components or products. Those filters come in varying shapes and roles. Some of them are network apparatuses filtering standard Internet protocol packets (such as firewalls); while others are small parts of integrated circuits filtering specific proprietary packets transiting on computer buses. Their common definition is: “a tool sitting on a communication channel, analyzing the sequence of packets (strings of bits with a beginning and an end) transiting on that channel, and potentially dropping, modifying or adding packets in that sequence”. Whenever the filtering algorithm applied is fixed for the lifetime of the component or product, this algorithm is often “hard coded” into the component or product with the potential addition of a configuration file allowing to slightly alter the behavior of the filter. However, sometimes the filtering algorithm to apply may depend on the deployment context, and may have to evolve during the lifetime of the component or product to adapt to new uses or attackers. In this case, it is often necessary to be able to easily G. Le Guernic, B. Combemale & J.A. Galindo 39 write new filtering algorithms for the specific product and context. Those algorithms are then often described using a Domain Specific Language (DSL) that is designed for the expression of a specific type of filters for a specific product. The definition of the syntax and semantics of this DSL is an important task. This DSL is the link between the filtering objectives and the process that is really applied on the packet sequences. Often, language specifications (when there is one) are provided using natural language. In the majority of cases, this leads to ambiguities or errors in the specification which propagate to implementations and final user code. This is for example the case for common languages such as C/C++ or Java™ [12]. “Unfortunately, the current specification has been found to be hard to understand and has subtle, often unintended, implications. Certain synchronization idioms sometimes recommended in books and articles are invalid according to the existing specification. Subtle, unintended implications of the existing specification prohibit common compiler optimizations done by many existing Java virtual machine implementations. [...] Several important issues, [...] simply aren’t discussed in the existing specification.” JSR-133 expert group [12] Some of those ambiguities, as the memory model of multi-threaded Java™ programs [12], required a formal specification in order to be solved. This paper is an industrial experience report on the use of a tool-supported language specification framework (the Kframework) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. The tool used to formally specify the DSL is introduced in Sect. 2. For confidentiality reasons, in order to be allowed by the DGA to communicate on this experimentation, the language specified for this experiment is not linked to any particular product or component. It is a generic packet filtering language that tries to cover the majority of features required by packet filtering languages. This language is introduced in Sect. 3 while its formal specification is described in Sect. 4. This language is tested in Sect. 5 by implementing and simulating a filtering policy enforcing a sequential interaction for a made-up protocol similar to DHCP. Before concluding in Sect. 7, this paper discusses the results of the experimentation in Sect. 6. 2 Introduction to the KFramework Surprisingly, even if it is a niche for tools, there exists quite a number of tools specifically dedicated to the formal specification of languages (our focus in this work is on specifying rather than implementing DSLs). Those tools include among others: PLT Redex [6, 13], Ott [23], Lem [19], Maude MSOS Tool [3], and the Kframework [20, 26]. All those tools focus on the (clear formal) specification of languages rather than their (efficient) implementation, which is more the focus of tools and languages such as Rascal [16, 2, 15] or its ancestor The Meta-Environment [14, 25], Kermeta [9, 10], and others. PLT Redex is based on reduction relations. PLT Redex is an extension (internal DSL) of the Racket programming language [7]. Ott and Lem are more oriented towards theorem provers. Ott and Lem allow to generate formal definitions of the language specified for Coq, HOL, and Isabelle. In addition, Lem can generate executable OCaml code. Ott is more programming language syntax oriented, while Lem is a more general purpose semantics specification tool. Ott and Lem can be used together in some contexts. The Maude MSOS Tool, whose development has stopped in 2011, is based on an encoding of modular structural operational semantics (MSOS) rules into Maude. Similarly to the Maude MSOS Tool, the K framework is based on rewriting and was also originally implemented on top of Maude. 40 Formal Specification of a Packet Filtering Language Using the K Framework The goal set for the experiment reported in this paper is to estimate the difficulty and benefits for an average engineer (i.e. an engineer with education and experience in computer science but no specific knowledge in formal language semantics) to use an “appropriate” tool for the formal specification of a packet filtering language. The “appropriate” tool needs to: be easy to use; be able to produce (or take as input) “human readable” language specifications; provide some level of correctness guarantees for the language specified; and be executable (simulatable) in order to test (evaluate) the language specified. The Kframework seems to meet those requirements and has been chosen to be the “appropriate” tool after a short review of available tools. As there has been no in depth comparison of the different tools available, there is no claim in this paper that the Kframework is better than the other tools, even in our specific setting. This section introduces the Kframework [21] by relying on the example of a language allowing to compute additions over numbers using Peano’s encoding [8]. The Ksource code of this language specification is provided below. 1module PEANO - SYNTAX syntax Nb ::= " Zero" |"Succ" Nb 3syntax Exp ::= Nb | Id | Exp "+" Exp [strict ,left] syntax Stmt ::= Id ":=" Exp ";" [strict (2) ] 5syntax Prg ::= Stmt | Stmt Prg endmodule 7 module PEANO imports PEANO - SYNTAX 9syntax KResult ::= Nb 11 configuration <env color ="green"> .Map </env > 13 <k color =" cyan"> $PGM :K </k> 15 rule N:Nb + Zero => N rule N1:Nb + Succ N2:Nb => ( Succ N1 ) + N2 17 rule 19 <env > ... Var :Id |-> Val:Nb ... </env > <k> ( Var:Id => Val :Nb ) ... </k> 21 rule 23 <env > Rho:Map (. Map => Var |-> Val ) </env > <k> Var :Id := Val:Nb ; => . ... </k> 25 when notBool ( Var in keys (Rho)) 27 rule <env > ... Var |-> ( _ => Val ) ... </env > 29 <k> Var :Id := Val:Nb ; => . ... </k> 31 rule S:Stmt P:Prg => S ~> P [ structural] endmodule G. Le Guernic, B. Combemale & J.A. Galindo 41 AKdefinition is divided into three parts: the syntax definition, the configuration definition, and the semantics (rewriting rules) definition. The definition of the language syntax is given in a module whose name is suffixed with “-SYNTAX”. It uses a BNF-like notation [1, 17]. Every non-terminal is introduced by a syntax rule. For example, the definition of the notation for numbers (Nb) in this language, provided on line 2, is equivalent to the definition given by the regular expression “(Succ)*Zero”. • Map env $PGM:K k Figure 1: Peano’s Kconfiguration The configuration definition part is introduced by the keyword configuration and defines a set of (potentially nested) cells described in an XML-like syntax. This configuration describes the “abstract machine” used for defining the semantics of the language. The initial state (or configuration) of the abstract machine is the one described in this configuration part. The parsed program (using the syntax definition of the previous part) is put in the cell containing the $PGM variable (of type K). For the Peano language, the env cell is used to store variable values in a map initially empty (.Map is the empty map). From this definition, the Kframework can produce a graphical representation of the configuration, provided in Fig. 1 The semantics definition part is composed of a set of rewriting rules, each one of them introduced by the keyword rule. In the Ksource file, rules are roughly denoted as “CCF => NCF” where CCF and NCF are configuration fragments. The meaning of “CCF => NCF” can be summarized as: if CCF is a fragment of the current abstract machine state (or configuration) then the rule may apply and the fragment matching CCF in the current configuration would then be replaced by the new configuration fragment NCF. In order to increase the expressivity of rules, CCF may contain free variables that are reused in expressions in NCF. If a specific valuation of the free variables Vin CCF allows a fragment of the current configuration to match CCF, then this fragment may be replaced by NCF where the variables Vare replaced by their matching valuation. The rules for addition over numbers (Nb and not Exp), on lines 15 and 16, follows closely this representation. For those rules, CCF is a program fragment that can be matched in any cell of the configuration. For those two rules, the Kframework can then produce the following graphical representations: RULE N:Nb + Zero N RULE N1:Nb + Succ N2:Nb (Succ N1)+N2 For other rules, the configuration fragment matching is more complex and involves precise configuration cells that are explicitly identified. In order to compress the representation, CCF and NCF are not stated separately anymore. The common parts are stated only once, and the parts differing are again denoted “CCFi=> NCFi”, where CCFiis a sub-fragment in CCF and NCFiis the corresponding sub-fragment in NCF. Cells that have no impact on a rule Rand are not impacted by Rdo not appear explicitly in the rule. Cells heads and tails (potentially empty) that are not modified by a rule can be denoted “...”, instead of using a free variable that would not be reused. For example, the rule which starts on line 18is the rule used to evaluate variables. The current configuration needs to contain a mapping from a variable Var to a value Val (“X |-> V” denotes a mapping from Xto V) somewhere in the map contained in the env cell. It also needs to contain the variable Var at the beginning of cell k. This rule has the effect of replacing the instance of Var at the beginning of cell kby the value Val. For this rule, the Kframework generates the graphical representation given in Fig. 2. The last rule on line 31 involves other internal aspects of the Kframework. It roughly states that, in order to evaluate a statement Sfollowed by the rest Pof the program, Smust first be evaluated to a 42 Formal Specification of a Packet Filtering Language Using the K Framework KResult (defined on line 9) and then Pis evaluated. 3 GPFL Context RULE Var:Id 7→ Val:Nb env Var:Id Val:Nb k Figure 2: Peano’s Krule for variables The language specified in the experiment reported in this paper, named GPFL, is a generic packet filtering language. For confidentiality reasons, GPFL is not a language actually used in any specific real product. GPFL has been made-up in order to be able to communicate on the experimentation on tool supported formal specification of filtering languages reported in this paper. However, GPFL covers the majority of features needed in packet filtering languages dealt with by the DGA. GPFL can be seen as the “mother” of the majority of packet filtering languages. GPFL aims at expressing a wide variety of filters. Those filters can be placed at the level of network, interfaces, or even communication buses between electronic components. They can be applied on standard protocols such as IP, TCP, UDP, . . . or on proprietary protocols, which are more common for component communication protocols. However, all those filters are assumed to be placed on a communication link. Messages (packets) that get through the filter can only get through in two ways, either “going in” or “going out”; there is no switching taking place in GPFL filters. Those different use cases are illustrated in Fig. 3. in out GPFL filter (a) Network filtering in out GPFL filter in out GPFL filter (b) Interface filtering in out GPFL filter in out GPFL filter (c) Bus filtering Figure 3: Use cases for GPFL-based filters GPFL focuses on the internal logic of the filter. Decoding and encoding of packets is assumed to be handled outside of GPFL programs (filters), potentially using technologies such as ASN.1 [11, 5]. For GPFL programs, a packet is a record (a set of valued fields). A GPFL program (dynamically) inputs a sequence of records and outputs a sequence of records. Figure 4 describes the architecture of GPFL- based filters. An incoming packet (on either side) is first parsed (decoded) before being handed over to G. Le Guernic, B. Combemale & J.A. Galindo 43 the GPFL program. If the packet can not be parsed, depending on the type of filter (white list or black list), the packet is either dropped or passed to the other side without going through the GPFL program. Any packet (record) output by the GPFL program (on either side) is encoded before being sent out. In addition, the GPFL program can generate alarms due to packets not complying with the encoded filtering policy. GPFL Filter Alarm Decoder Encoder DecoderEncoder bin bin P o r t P o r t white list black list white list black list Figure 4: Architecture of GPFL-based filters The GPFL language must allow to: drop, modify or accept the current packet being filtered; generate new packets; and generate alarms. GPFL must allow to base the decision to take any of those actions on information pieces concerning the current packet being filtered and previously filtered packets. Those information pieces must include: some timing information, current or previous packets directions through the filter (“in” or “out”), and characteristics of current or previous packets including field values and computed properties such as, for example, a packet “type” or total length. The computation of those properties and decoding of packet fields is outside of the scope of GPFL; it is left to the decoders. In order to gradually build a decision, GPFL must allow to interact with variables (reading, writing, and computing expressions) and automata (triggering a transition in an automaton and querying its current state). The intent for automata is to be used to track the current step of sessions of complex protocols. GPFL must allow to combine filtering statements using: sequential control statements (executing two statements in sequence); conditional control statements (executing a statement only if a condition is true); iterating control statements (repeatedly executing a statement for a fixed number of repetitions). There is no requirement for a loop (or while) statement whose exit condition is controlled by an expression recomputed after every iteration. For the experiment reported in this paper (on formal specification of a filtering language), the iterating statement is considered sufficient for the intended use of GPFL and close enough to a loop statement from a semantics point of view, while exhibiting interesting properties for future analyses (for example, any GPFL program terminates). 4 GPFL’s Specification Due to lack of space, GPFL’s specification and testing is only summarized in this paper. However, a full specification of GPFL and a testing section can be found in the companion technical report [18]. 44 Formal Specification of a Packet Filtering Language Using the K Framework Syntax. To the exception of expressions and expression fragments, GPFL’s syntax is formally defined by the Ksource fragment provided below. 18 syntax Cmd ::= " nop" |"accept" |" drop" |" send (" Port "," Fields ")" |" alarm (" Exp ")" [strict(1)] 20 |"set(" Id "," Exp ")" [strict(2)] |"newAutomaton(" String "," AutomatonId ")" 22 |"step (" AutomatonId "," Exp "," Stmt ")" [strict(2)] syntax Stmt ::= Cmd 24 |"cond (" Exp "," Stmt ")" [strict(1)] |"iter (" Exp "," Stmt ")" [strict(1)] 26 |"newInterrupt(" Int "," Bool "," Stmt ")" | Stmt Stmt [right ] 28 |"{" Stmt "}" [bracket] 30 syntax AutomataDef ::= " AUTOMATA " String AutomataDefTail syntax AutomataDefTail ::= " init " "=" AStateId ATransitions | ATransitions 32 syntax ATransitions ::= List{ATransition ,""} syntax ATransition ::= AStateId "-" AEvtId " ->" AStateId 34 syntax AStateId ::= String syntax AEvtId ::= String 36 syntax InitSeq ::= "INIT " Stmt syntax PrologElt ::= AutomataDef | InitSeq 38 syntax Prologues ::= PrologElt | PrologElt Prologues 40 syntax Program ::= " PROLOGUE " Prologues "FILTER" Stmt A GPFL program is composed of a prologue, executed only once in order to initialize the execution environment, and a filter statement, executed once for every incoming packet. A prologue is composed of automaton kind definitions and initialization sequences. An automaton kind definition specifies an identifier K, an initial state for automata of kind Kand a set of transitions for automata of kind K. A transition definition is composed of: two automaton states Fand T, and an automaton event that triggers the transition from Fto T. A GPFL statement is composed of GPFL commands or statements combined sequentially. Some statements can be guarded by an expression and executed only if that expression evaluates to true (cond). Some statements (iter), associated with an expression e, are exectued vtimes, where vis the value of ebefore the first iteration. Finally, newInterrupt statements register a statement to be executed in the future, potentially periodically. GPFL commands are the basic units having an effect on the execution environment. The nop command has no effect and serves mainly as a place holder. The accept, resp. drop, command states to accept, resp. drop, the current packet and stop the filtering process for this packet. The send command sends a packet on one of the ports. The alarm command generates a message on the alarm channel. The set command sets the value of a variable. The newAutomaton command initializes an automaton of the provided kind, and assigns this newly created automaton to the provided identifier. The step command tries to trigger an automaton transition by sending an event eto an automaton a. If there is no transition from the current state of atriggered by the event e, then the associated statement is executed. Semantics The full formal specification of GPFL’s semantics can be found in the companion technical report [18]. GPFL’s semantics rules are defined on the configuration presented graphically in Fig. 5. The prg cell contains the GPFL program. After initialization of the program, automaton kind definitions are stored in the automatonKindDefs cell and the filter cell contains the filter (GPFL statement) G. Le Guernic, B. Combemale & J.A. Galindo 45 $PGM:K prg • K automataKind • K initialState • Map transitions automataKindDef* automataKindDefs • K filter • List nextInterrupts • K intTime • K intCode • K period interrupt* interrupts • K k 0 clock • K inHead • List inTail in • List alarm • List out streams • K time • K port • Map fields input • Map kinds • Map states automata • Map vars env Figure 5: Kconfiguration of GPFL that is to be executed for every packet. The interrupts cell contains a set of interrupt definitions (interrupt*). An interrupt is a triplet composed of: the time when the interrupt is to be triggered, the code (statement) to be executed, and a “Time” value equal to the interruption period for a periodic interruption (or nothing for a non-periodic interruption). In addition, the interrupts cell contains an ordered list of the next “times” when an interrupt is to be executed. The clock cell registers the current “time”. The configuration also contains a kcell that holds the GPFL statement under execution. Each time a new packet is input, the content of the kcell is replaced by the content of the filter cell, and the newly arrived packet is stored in the input cell with its arrival time and port. Packets are input from the streams cell which contains: the packet input stream divided into the next packet to arrive (inHead) and the rest of the stream (inTail); the packet output stream; and the alarm output stream. In the input stream, resp. output stream, packets arriving, resp. leaving, on both 46 Formal Specification of a Packet Filtering Language Using the K Framework ports are mixed together, but contains information on the port of entry, resp. exit. Some choices made to represent those streams are not an intrinsic part of GPFL’s formal specification. The division of the input stream into a head and a tail is such a choice. Those choices are made in order to be able to execute the specification. It is then required to implement, in the Kframework, a mechanism to retrieve and parse strings describing packet sequences sent to the filter. In order to help distinguish between the formal specification of GPFL and the mechanisms put in place to execute it, whenever possible, implementation choices, such as the format of strings describing packets, are defined in another file which is loaded in the main specification file with the require instruction. Finally, the env cell is the main dynamic part of the execution environment. It corresponds to a “record” of maps that associate: automaton kind and current state to automaton identifiers (automata cell); and values to variables. 5 Testing GPFL’s Specification GPFL’s specification, introduced above and contained in the companion technical report [18], is not necessarily perfect. By a matter of fact, imperfections of GPFL’s specification are of interest to the experimentation reported in this paper. Indeed, the goal of the experimentation is to see how a tool such as the Kframework can help to spot and correct imperfections in filtering language specifications. One way to do so is by “testing” the new language specified, which is possible if the framework used to specify the language supports the execution or simulation of language specifications, which is the case for the Kframework. The test scenario used assumes a network of clients and servers. The clients request resources to servers using a made-up protocol, called “DHCP cherry”, summarized in Fig. 6. The test scenario as- Server Server 1 Client Client Server Server 2 Disc Disc Off(R1) Off(R2) Req(R1) Rej(R2) locks R1 Ack Ack msc Nominal acquire sequence Server Server 1 Client Client Rel(R1) unlocks R1 Ack msc Nominal release sequence Figure 6: Nominal packet sequences of DHCP cherry protocol sumes that servers behave poorly when interacting concurrently with different clients. The objective of the test scenario is then to filter communications in front of servers in order to prevent any concurrent client-server interactions with any given server. This test scenario is obviously made-up for this experimentation, which is a requirement due to confidentiality issues. However, it is still covering the most frequently used features of filtering languages similar to GPFL, while remaining simple enough for a first experimentation.