description of the interface behaviour of each container, the tool builds a formal model of the overall system, which can be verified in ProVerif (an automatic symbolic protocol verifier), to check that the overall system satisfies the required properties. The system can be described in a specification language capable to express at once the interfaces and connections of containers and the relevant behavioural aspects of their interfaces, called JSON Bigraph Format (JBF), and inspired by previous formal models, based on bigraphs, for containerized architectures.
In this work, we present the design and prototype implementation of such a tool, called
DBCChecker, whose aim is to verify security properties of systems obtained by the composition
of containers. More precisely, given a configuration of a container-based system and for each
container an abstract description of the interaction on its interface (i.e., a contract), the tool
assembles these information into a formal model of the overall system. Then, this model is
fed to a verification backend (in our case, ProVerif [
This work leverages previous results on formal models for containerized architectures based
on bigraphs [
However, interfacing these libraries with containers configurations on one hand, and with protocol verifiers on the other, requires some ingenuity; in particular, we have to introduce a specification language capable to express at once the interfaces and connections of containers (like in bigraphical model) and their contracts; from these specifications DBCChecker can build the input model to be fed to the backend verifier (i.e., ProVerif). This language is called JSON Bigraph Format (JBF), and it is based on JGF, the standard JSON Graph Format.
This paper is structured as follows. In Section 2 we recall the bigraphical models of containers. Based on it, in Section 3 we introduce the specification language JBF. These specifications are the inputs of DBCChecker, which is presented in Section 4. In Section 5 we provide two examples of verification of security properties of systems obtained by container compositions. Finally, in Section 6 we draw some conclusions and sketch directions for further work.
DBCChecker is open source and available at https://github.com/cysecud/DBCChecker.
The formal model for containter-based systems is based on local directed bigraphs [
A (local) interface = ⟨(0+, 0− ), (1+, 1− ), . . . , (+, − )⟩ is a list of polarized interfaces, each of which is defined as a pair of disjoint finite sets of names (+, − ). The pair (0+, 0− ) contains the global names. We define + ≜ ⨄︀=1 + and − ≜ ⨄︀=1 − , ℎ() ≜ .
Two interfaces , can be juxtaposed yielding a new interface, as follows: ⊗ ≜ ⟨(0+ ⊎ 0+, 0− ⊎ 0− ), (1+, 1− ), . . . , (+, − ), (1+, 1− ), . . . , (+, − )⟩ A signature defines the basic building blocks of a bigraph; in our case, these will represent processes, containers, networks, etc.. Formally, a signature is a set of elements ∈ , called controls, each with a polarized arity = ⟨+, − ⟩; intuitively, these represent the input and output ports of the control, respectively.
container process request network volume
Given a signature, we can consider bigraphs built using these basic blocks. A local directed bigraph (ldb) : → is a tuple = (, , , , ), where • and are the inner and outer interfaces respectively; • and are the sets of nodes and edges respectively; • : → is the control map, assigning a control type to each node of the bigraph; • : ℎ() ⊎ → ⊎ ℎ() is the parent map, representing the hierarchy between nodes and their position in the external interface; • : () → () is the link map, connecting points (i.e., positive ports on nodes and inward names on interfaces) to links (i.e., negative ports and outward names).
Let 1 : 1 → 1, 2 : 2 → 2 be two ldb. Their juxtaposition 1 ⊗ 2 : 1 ⊗ 2 → 1 ⊗ 2 is defined as 1 ⊗ 2 = (1 ⊎ 2, 1 ⊎ 2, 1 ⊎ 2, 1 ⊎ 2, 1 ⊎ 2).
Let 1 : → , 2 : → be two ldb. Their composition 2 ∘ 1 : → is defined as the bigraph (1 ⊎ 2, 1 ⊎ 2, 1 ⊎ 2, , ), where : ℎ() ⊎ → ⊎ ℎ() and : (2 ∘ 1) → (2 ∘ 1) are defined as expected.
Thus, (directed) bigraphs can be seen as particular data structures, parametric in the given signature. Several tools and libraries have been implemented for representing and manipulating these data structures, see e.g. [9, 11, 10], and in particular JLibBig (https://bigraphs.github.io/ jlibbig/), a Java library for bigraphs which is the basis of the current work [12].
Now that we have defined the algebraic framework of our model, we can introduce a signature
for containers. The signature we consider in this paper is the one presented in [
A relevant example of bigraph composition is given by the composition of containers, as
performed by, e.g., docker compose. In this case, the context bigraph can be obtained
automatically from the docker-compose.yml file. As an example (taken from [
0 80 80 80 80
/var/www/data 80 front
lmysql wp /var/www/data 80 front
lmysql wp 0 0 lmysql lmysql 4.4. Propriet`a di consistenza 4.4.2
8080 wp Condivisione di reti front front db back db back 3306 front
back 3306 front back db db 0 0 3306 Figurafr4o.n35t3:06Edsaetmavpoioludmiecomposizione.
back Figura 4.5: Esempio di composizione.
db back pma back pma /data /data 80 80 80 back
lmysql pma 80 back
lmysql pma /data /data 0 0 80 80 lmysql lmysql pma 8181
23 4. Formalizzazione dei Container come Bigrafi diretti con localit`a
datavolume front db 1front db 1 datavolume back back 2 2 pma pma 8181 8181 A4l.t4ra.2possCiboilnedsiitvuiasziioonnee ddi ierrreotrie `e quella in cui si e ettua una links tra due container, ma questi non condividono nessuna rete. In questo caso dev’essere riportato un errore all’utente. L’esecuzione in questo Altra possibile situazione di errore `e quella in cui si e ettua una links tra due container, ma questi non 0 1 2 caso produrrebbe dei risultati inconsistenti. Docker Compose non e ettua alcun controllo sulla verifica condividono nessuna rete. In questo caso dev’essere riportato un errore all’utente. L’esecuzione in questo di questa condizione. caso produrrebbe dei risultati inconsistenti. Docker Compose non e ettua alcun controllo sulla verifica
Tramite bigrafi questa proprieta` `e verificabile garantendo che ogni container che e ettua una links di questa condizione. abbia almeno un nome di rete in comune con quelli del controllo a cui si collega. Siano c e d due
Tramite bigrafi questa proprieta` `e verificabile garantendo che ogni container che e ettua una links caob(ncbt)riaollailrmelea8nt0oiviuanldmnuoyesmqcleondtiairneetrecionnnceosmsiu3dn3ae0u6cnoan liqnukesl,lindetecl econnettrdollo a cui si collega. Siano c e d due gli insiemi deilmnyosmqli de8l0le reti di c e d, rispettivamente. A nch´e la proprieta` sia garantita deve valere: netgclfli innseitedm”=i d?e.i nNoemlbiidgerlalefore`etpiodsiscibeiled, controlli relativi a due container connessi da una links, net e net Figure 4: Ecoxsatmruipreleqouefsctioimnspieomsiitaiopnar:tFi(raieg)udtrahaien4.oc6do:i mIdl ipbtoiigpsroiatficooodnnotapeinonevlarci.rcoonmmpdoesniztio(nceo.rresponding to the YAML file in Figure 3); (b) the containers to be assembled; (c) the resulvtaolefret:hneetccofl mnpetods” ition.
rispettivamente. A nch´e la proprieta` sia garantita deve = ? . Nel bigrafo `e possibile scvoosltgreuirqeueqsuteosttii pinosidemiainaapliasirtairepadratiirneoddiadui ntipboigcraofnotaminoedr.ellante un file di configurazione di Docker 4.4.3 Gerarchia delle reti
Compose. 3.
JBF AS4.fip4n.i3edicsGiicfueirrecazrzacahtpiioatordenbeblleelrariseuntltigareunaecegsseario che nel proprio sistema, in presenza di piu` reti, si voglia garantire che queste non entrino in contatto, per evitare fughe di informazioni non desiderate. Un A fini di sicurezza potrebbe risultare necessario che nel proprio sistema, in presenza di piu` reti, si voglia In order teosemmpaiokpeottrhebebewehssoerleeqsuyelslotedmiunsacsacluaoblal.eP,emreosdemupliaordaalnladrettoe daelllleoawulefousrattehdeaicroagnaszezirnvoantion of garantire che queste non entrino in contatto, per evitare fughe di informazioni non desiderate. Un informatiodnevse, einsscerleucdoinnsegnttihtooascecendeoret narelelsapsurrneetoesednegtlaibuleciipnameramabitntiiugstarrraaetpiuvhni,a,mi.een.t,rethilevibceevherasvai`eoluecritoo.mfoadenlloode in a
Docker Compose non o re strumento simile verifica. Tramite bigrafico `e possibile e ettuare questo controllo. Nella sezione 6.2.2 viene presentato un algoritmo che communicatiDoonck.eWrCeomwpaonset ntohniso lraenngeussaugnoe sttorubmeenbtoaspeerdaottnuaare sutnaansdimarilde vseprieficcaific.aTtriaomnitleamnogduealloge, in order to imbpigrraofivceo `ceopmosspibaitleibeileitttyu.aFreuqrutehsetor mconotrreollwo.eNwellaansetztiohnies 6l.a2n.2gvuieange eprteosebnteateoxupnraelsgsoirvitemoe nchoeugh to be able to descrive a broad class of behaviours.
We thus introduce the JSON Bigraph Format ( JBF). This language is based upon the JSON Graph Format ( JGF) [15], which is a standard format for graph structures: it allows us to describe nodes, edges and the metadata of graphs. JBF leverages on these metadata objects to describe the signature and other specific informations of directed bigraphs, while the bare structure of JBF (Fig. 5a) is the same as JGF’s for compatibility with the standard.
"graph": { "nodes": {}, "edges": [], "type": "ldb", "metadata": {
"signature": {} } }
(a) Bare structure 1 "siteId": { 2 "metadata": { 3 "type": "site" 4 }, 5 "label": "siteId" 6 }
(d) Site structure
In Fig. 5b it is shown the node structure: we use metadata objects to describe the node properties that are not representable in JGF (e.g. the type of the node, its control and the data needed for security checks). The label object is used to give a meaningful name to the node.
The root structure is provided in Fig. 5c. The location object must be a progressive integer from 0 to , where 0 is the global location. Likewise, we describe sites (Fig. 5d).
In Fig. 5e we focus on the name structure. The interface object must be either “outer” or “inner”. The locality object has the same role it has in the root structure. The polarity object must be “+” or “-”: a “+” indicates an outgoing edge in an outer interface and an ingoing edge in an inner interface, while a minus means the opposite.
There are two types of edges in JBF: Place Relationships and LinkedTo Relationships. For the Place Relationship structure (Fig. 5f) we reuse the JGF default fields. The source and target objects identify the parent and son IDs. The relation object must be set to “place" to indicate that the edge we are describing is a place relationship. The metadata object must be empty.
In Fig. 5g we show the LinkedTo Relationship structure: we have to use the metadata object to describe the information that can not be represented in standard JGF. The relation object must be of value “linkedTo". The portFrom and portTo objects must be progressive integers and they represent the ports used by the source and the target for the connection. If a name is involved in the connection the port must not be specified since names do not have ports.
The Control structure is shown in Fig. 5h: it is part of the signature object inside the metadata of the bigraph. This allows us to deviate from the standard JGF specification in order to describe the control of the bigraph. The active object is a boolean that indicates whether the control is active or not. The arityOut and arityIn objects must be progressive integers and they represent the cardinality of outgoing and incoming edges of the control.
Protocol specification Since we want to keep the standard provided by JGF unchanged, we could not express all the properties necessary for the security checks in a single JSON ifle. Instead, we create an extension to the JBF specification which allows us to describe the remaining properties. This extension takes the form of a separate JSON file. If we want to verify the security properties of a directed bigraph, we need to provide to the system both its JBF specification and its extension.
The bare structure of this extension is provided in Fig. 5i. The bigraphInfo object is used to set the unique ID of the bigraph so as to simplify the identification of the bigraph and its storing in a database. The types object is used to declare the types used in the verification process. The variables object is used to declare the variables which could be both public and private. The functions object is used to declare the functions while the queries object is used to declare the queries which can be of three types: “query”, “attacker” and “equation”. The instantiations object is used to declare the instantiations of the variables, in order to relate the abstract variables to the concrete ones. Finally, the prologue object can be used to declare code that will be executed before the main process in the verification backend.
As shown in the previous sections, when it comes to representing a container system, bigraphs are a natural choice. The JLibBig library is the ideal candidate for representing and manipulating bigraphs due to its flexibility and extensibility. However, to fulfil our specific needs, we have extended JLibBig by adding new features, including an Import/Export feature and a Verification feature, which are divided into five modules, as depicted in Fig. 6.
The Import/Export functionality is facilitated by the I/O module, which is one of the most important components of our system. It is responsible for importing and exporting Bigraphs in a standard format, specifically the JSON Bigraph Format (JBF) which we have defined in Section 3. The I/O module is designed to be used independently of the verification functionality. Furthermore, to make sure that it remains as general as possible and not limited to our specific
Core Module
purposes, we have set up extension points, often represented by interfaces, which can be used to extend the Import/Export functionality to bare bigraphs.
The Networking module is a service component that manages all communications between the library and external components, including the user. To ensure portability and isolation, all communications are performed through REST methods.
The Parsing module extends the Import/Export module and is responsible for parsing additional information from the directed Bigraph necessary for security checks, and represented in the JBF extension described in Section 3.
The Translation module is responsible for translating the parsed information into a file that can be processed by ProVerif. This step is critical as it is the connection point between Bigraphs and ProVerif. Furthermore, our system is modular and can be adapted to diferent verification backends. This can be achieved by suitably modifying the Translation module, in order to produce models for alternative protocol verifiers. Given the relevance of this moduel, in Fig. 7, we provide an UML describing the flow of the parsing and translation process. When the User wants to verify a system, he provides the two JBF to the system. The core parsing module extracts the standard properties of the system and creates a Bigraph Object, while the parsing module specific for security properties parses the behaviour of every node and all the other related properties and save them in records. Lastly the Translation module use these records to create the input file in ProVerif language (.pv). When the file is created the translation is completed and the tool can call ProVerif and check the security properties of the system.
The Verification module is the main actor and controller of our system, responsible for the entire verification process. It uses all the previous modules except the I/O module which is unrelated to the verification process. In Fig. 8, we provide a sequence diagram of a verification request. When the User ask for a verification, if the data contain errors, then the system terminates the operations returning an error. Otherwise, it will process the data, constructs a complete model of the container system, and sends it to the backend (ProVerif) to start the security checks. Once the verification is complete, ProVerif sends the result to the system, which could be either a success or an error. Then the system forward the result to the user.
The verification module calls the Parsing Module to parse the directed bigraph security properties. If the parsing succeeds, the verification module calls the Translation Module to JBF
JBF Integrative
Verification Module
Verify
Parsing Module Specific for ProVerif
Create Input ParseInput writes records
reads
Parsing Module Core ParseInput
ParseSignature ParseNode
ParseEdge
Translation Module
File ProVerif .pv create a file for ProVerif, which is then sent to the backend for verification. Then, once the Networking Module has received the result of the verification, it sends it back to the Verification Module, which returns the result to the user.
clientA #0 serverB clientA
serverB (, (, (, ))) (, )
To demonstrate the use of the DBCChecker and JBF, in this section we provide two simple example applications. 5.1. Verification of a cryptographic handshake In this first example, we deal with a simple handshake protocol between two containers, a client and a server , over a shared channel. The bigraphical model of this setting, and a sequence diagram of the protocol, are shown in Fig. 9. Informally, the protocol proceeds as follows: 1. sends its public key to . 2. generates a random key , and sends it back to signed with his private key and encrypted using the public key received received at step 1. 3. decrypts the key using her secret key , and checks the signature using the (known) public key ; if this succeeds, uses to encrypt and send a secret message to . The security property we want to check is that an attacker (e.g., the host or another container), observing the trafic between the two containers, cannot obtain .
Fig. 10 depicts a portion of the JBF structure. Most of the information conveyed by JBF is contained within the “metadata" object, as the node is responsible for its own behaviour and information. In this case, we have a short fragment in applied -calculus (the specification language of ProVerif) abstractly describing the steps that each container will perform.
Fig. 11 shows the complete structure of the JBF Integrative file, which contains all the information required by ProVerif for verification that is not specific by any node. This separation facilitates the combination of multiple nodes by simply modifying the JBF Integrating file. In particular, this file declares also the security property(ies) to be proved (lines 13—15).
To verify this system of containers, the process is straightforward. The user creates two JSON ifles needed for the verification: one containing the description of the system (JBF) and one with the information necessary for the verification with ProVerif (JBF Integrative). These files can be created from scratch or composed and built upon existing files, since it is the container itself, within the “behaviour” field, which contains the logic of its behaviour. Subsequently, the user can submit the files to DBCChecker, which verifies the whole system obtained by the composition, and provides the user with the result of the ProVerif verification.
In this case, ProVerif finds an attack on , providing also the execution trace that an attacker can follow to obtain , as shown in Fig. 12. In this attack trace ProVerif shows that the protocol examinated is vulnerable to Man in the Middle Attacks. The Attacker pretends to be clientA towards serverB and vice versa, so that, when the serverB sends the session key the attacker obtain it and, in the next step decrypts the secret message sent by clientA.
!
! Beginning of process clientA Beginning of process serverB
A trace has been found.
Honest Process 5.2. Verification of information leakage between containers In this example, we consider two containers that communicate over a private shared channel. The exchange is trivial: the client sends to the server a secret piece of information. The bigraphical model of this scenario is shown in Fig. 13. We define the containers contracts using JBF, a partial view of which is given in Fig. 14.
The global property we want to check is that no attacker can obtain the secret .
Since the channel is private (i.e. not exposed to any attacker), the property is trivially verified, as confirmed also by DBCChecker: the query is verified by Proverif, as shown in Fig. 15.
Let us suppose we want to add another functionality to the system, e.g., we want to log the requests from the client to the server for legal compliance reasons. This can be accomplished by adding a new container that listens on the same network where the client-server exchanges are made and publishes, on another network, a log entry for each request. The new bigraphical model is shown in Fig. 16. The actual logger implementation is not fixed: diferent contracts can lead to diferent system behaviour, some of which may prove problematic.
Let us suppose the contract specification of the logger we want to introduce is the one in Fig. 17. Since this implementation writes the entire request to the public channel, the secret is leaked. This can be seen by the attack trace in Fig. 18. To solve this problem it is necessary to choose another logger that, e.g., does not leak the entire request. This is well-known in the industry; for example the standard logger for GitHub Actions scans the log message body for GitHub Secrets and removes them from the final output. #0
This example shows that composing containers is a complex and dangerous operation: we started with a secure container system and we added another container, which is not malicious per se. While apparently the composition is safe, DBCChecker proves that it is not: the extended system violates the security property that the original one satisfies.
In this work, we have presented DBCChecker, a prototype tool for verifying security properties of systems obtained by composition of containers. To this end, we have introduced a specification language, called JSON Bigraph Format (JBF), inspired by formal models for containerized architectures based on bigraphs. This formalism is capable to express at once the interfaces and connections of containers and the relevant behavioural aspects of their interfaces. From these specifications, the DBCChecker tool builds a model of the overall system, which can be verified in ProVerif, to check that the overall system satisfies the required properties.
Future work. We are currently working on adding support for other kinds of bigraphs using the extension point and the interfaces we have prepared in this work. Another possibility is to add support for quantitative aspects, taking advantage of stochastic semantics and the algorithm for computing optimal embeddings implemented in jLibBig [12, 16, 17].
Another important goal is simplifying the user interaction with the tool and help the modelisation of the container network. At the moment DBCChecker does not ofer an easy way to A trace has been found.
Honest Process model complex systems: the implementation of a GUI could be a major step towards a complete and user-friendly toolkit. Along this line, another improvement would be to integrate the system with a network discovery tool, in order to simplify the process of modelling and verifying large and dynamic containers based systems. This would result in a semi-automatic bigraph creation, allowing the user to concentrate upon formalizing the security properties to be verified.