We describe work on the formal verification (using SMT solving and symbolic model checking) and on the synthesis of chains of networking functions intended to limit the ability of mobile applications to carry out attacks on servers and networking infrastructure. In order to generate a chain dedicated to a particular application, we learn a Markov chain representing the networking activity based on network flows captured on-device. Rules expressed as Horn clauses that take into account the structure of the Markov chain and threshold parameters provided by network operators classify the network activity according to different types of attacks and infer predicates indicating which network rules should be deployed. Chains for individual applications are merged into a single chain and then optimized for deployment in a given network infrastructure. The resulting chains are expressed in Pyretic, a domain-specific language for programming software-defined networks and can be deployed in a cloud infrastructure. Preliminary experiments in a network simulator indicate that the proposed approach for synthesizing and deploying security chains appears feasible, although the precision of detecting attacks is not yet satisfactory for all types of applications.
Joint work with Nicolas Schnepf, Rémi Badonnel, and Abdelkader Lahmadi