Biblio

Today's Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol's authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.

Internet of Things is nowadays growing faster than ever before. Operators are planning or already creating dedicated networks for this type of devices. There is a need to create dedicated solutions for this type of network, especially solutions related to information security. In this article we present a mechanism of security-aware routing, which takes into account the evaluation of trust in devices and packet flows. We use trust relationships between flows and network nodes to create secure SDN paths, not ignoring also QoS and energy criteria. The system uses SDN infrastructure, enriched with Cognitive Packet Networks (CPN) mechanisms. Routing decisions are made by Random Neural Networks, trained with data fetched with Cognitive Packets. The proposed network architecture, implementing the security-by-design concept, was designed and is being implemented within the SerIoT project to demonstrate secure networks for the Internet of Things (IoT).