This blog post is written by Matteo Pradella and Andrea Franchini
Model checking is a formal verification approach where a system is typically represented as an operational model, together with a logical framework for expressing and checking that certain desired properties are guaranteed, or whether undesirable situations may occur. Traditionally, systems are modeled with some variants of automata, graph or transition system, which are natural representations for evolving stateful systems such as electronic devices or imperative programs. [citation on Model Checking, e.g. some manual][MP1] [Ug2]
Recently, techniques involving SAT (Boolean Satisfiability) and SMT (Satisfiability Modulo Theory) solvers appeared. They leverage advancements in algorithms for SAT (such as DPLL) to provide tools that are often very fast on practical models, despite the theoretical complexity bounds (e.g. SAT is a well-known NP-complete problem). Model checkers based on these tools typically translate the original model into the chosen logic, namely propositional logic for SAT, more complex first-order theories for SMT. This approach is very flexible; hence it is used in #PIACERE for translating the IaC model, written in the #PIACERE DOML language, into the language provided by Z3, one of the most used SMT solvers [cite Z3].
The current version of #PIACERE Model Checker targets the DOML language and is integrated with the IDE. It receives the DOML file from the IDE and checks it against a set of built-in requirements. For example, it can verify that two services in a producer-consumer relationship, like a Web Server and its DBMS, must be able to communicate across a network in the deployment configuration. When a model does not satisfy the model checker requirements, an error message alerts the user of what is wrong in the model, and it tries to be as descriptive as possible, highlighting the cause.
The Model Checker has recently been extended to support user-supplied requirements written in a simple DSL to verify additional properties, when needed. The DSL is minimalistic and allows user to specify properties about DOML elements and their relationships through a natural first-order logic.
Example
We now present an example of how the model checker behaves. In the following DOML, we want to deploy a simple web server hosting a blog, that fetches its contents from a database.
We define in the application layer the two services, specifying that the web server myBlog_nginx depends on the DBMS myDb.
doml blog_example
application blog {
software_component myBlog_nginx {
consumes { sql_connection }
}
dbms myDb {
provides { sql_connection }
}
}
In the infrastructure layer, we define two virtual machines that will respectively host the web server and the DBMS. The two VMs (webVM, dbVM) must be able to communicate, so we connect them on the same network myNet.
infrastructure infra {
vm webVM {
iface webIface {
belongs_to myNet
security webSG
}
loc { region “europe” }
}
vm dbVM {
iface dbIface {
belongs_to myNet
security dbSG
}
loc { region “europe” }
}
net myNet {
protocol “tcp/ip”
cidr “192.168.1.0/24”
}
We also define two security groups to restrict inbound connections on the two VMs; in particular, we allow HTTP and HTTPS connections for the web server, and MySQL connections on port 3306 for the DBMS.
security_group webSG {
ingress http {
from_port 80
to_port 80
protocol “tcp”
cidr [“0.0.0.0/0”]
}
ingress https {
from_port 443
to_port 443
protocol “tcp”
cidr [“0.0.0.0/0”]
}
}
security_group dbSG {
ingress mysql {
from_port 3306
to_port 3306
protocol “tcp”
cidr [“0.0.0.0/0”]
}
}
}
We then map the application components onto the infrastructure components, specify it as the active deployment. We also add a concrete infrastructure mapping the abstract infrastructure element we defined above and minimal optimization layer.
deployment myDepl {
myBlog_nginx -> webVM,
myDb -> dbVM
}
active deployment myDepl
concretizations {
concrete_infrastructure con_infra {
provider example_provider {
vm concrete_webVM { maps webVM }
vm concrete_dbVM { maps dbVM }
net concrete_net { maps myNet }
}
active con_infra
}
optimization opt {
objectives {
“cost” => min
“availability” => max
}
}
Running the model checker, we get that the model satisfies all built-in requirements.
Let’s now try to remove the network interface from the webVM component, in the infrastructure layer.
vm webVM {
//iface webIface {
// belongs_to myNet
// security webSG
//}
loc { region “europe” }
}
Running the model checker again we get the following error message:
There are 3 unsatisfied requirements, and their error messages are the following:
- “Virtual machine webVM is not connected to any network interface.” This is caused directly by the code we have deleted. In almost most situations, a VM should always be connected to a network to communicate.
- “Software components myDb and myBlog_nginx are supposed to communicate through interface sql_connection, but they are deployed to nodes that cannot communicate through a common network.” Because we have specified in the application layer that the web server depends on the database, there must be a connection between the two on some network. Since webVM does not have an interface, communication is not possible.
- “Security group webSG is not associated with any network interface.” We have defined a security group that is not used by any interface since it was associated with the interface we deleted.
The user can fix these issues starting by adding a network interface to the webVM element, and associating it correctly to the other DOML elements (Security groups, networks).
Let’s say we have a requirement that is not between the built-in ones, for example we want the infrastructure to reside in Europe. We can leverage the location block of the virtual machine element and its region property to write that requirement.
Inside the functional_requirements layer we can write additional requirements. The syntax for the DSL is explained in detail here [https://piacere-model-checker.readthedocs.io/en/latest/writing-requirements.html].
In plain english, we want to specify that: for each virtual machine, it must exist a location element in that VM such that its attribute ‘region’ is equal to ‘Europe’.
functional_requirements {
Req1 “`
+ “All VM have a location, and location is ‘europe'”
forall vm (
vm is class abstract.VirtualMachine
implies
exists loc (
vm has abstract.ComputingNode.location loc
and
loc has abstract.Location.region == “europe”
)
)
error: “VM does not have location or location is not europe.”
“`;
}
Running again the model checker, we get that this requirement is satisfied, because it does not appear in the error message (if any). If we try to remove the location (loc) attribute from a virtual machine or change the region value to something else (e.g. ‘China’), we get the following error message, as expected.
vm dbVM {
iface dbIface {
belongs_to myNet
security dbSG
}
loc { region “china” }
}
All developed prototypes are open source and publicly available. Documentation is available at: https://piacere-model-checker.readthedocs.io/
0 Comments