Ensuring that information flowing through a network is secure from manipulation and eavesdropping by unauthorized parties is an important task for network administrators. Many cyber attacks rely on a lack of network-level information flow controls to successfully compromise a victim network. Once an adversary exploits an initial entry point, they can eavesdrop and move laterally within the network (e.g., scan and penetrate internal nodes) to further their malicious goals. In this article, we propose a novel multilevel security (MLS) framework to enforce a secure inter-node information flow policy within the network and therein vastly reduce the attack surface available to an adversary who has penetrated it. In contrast to prior work on multilevel security in computer networks which relied on enforcing the policy at network endpoints, we leverage the centralization of software-defined networks (SDNs) by moving the task to the controller and providing this service transparently to all network nodes. Our framework, MLSNet, formalizes the generation of a policy compliant network configuration (i.e., set of flow rules on the SDN switches) as network optimization problems, with the objectives of (1) maximizing the number of flows satisfying all security constraints and (2) minimizing the security cost of routing any remaining flows to guarantee availability. We demonstrate that MLSNet can securely and efficiently route flows that satisfy the security constraints and route the remaining flows with a minimal security cost (e.g., route >85% of flows, where the heuristic achieves 89% and 87% of the optimal solutions for the optimization problems).

IoT systems are revolutionizing our life by providing ubiquitous computing, inter-connectivity, and automated control. However, the increasing system complexity poses huge challenges for security as IoT devices are distributed, highly heterogeneous, and can directly interact with the physical environment. In IoT systems, bugs in device firmware, defects in network protocols, and design flaws in automation rules can lead to system breach or failure. The challenge gets even more escalated as the possible attacks may be chained together in a long sequence across multiple layers, rendering the existing vulnerability analysis frameworks inapplicable. In this paper, we present FORESEE, a model checking-based framework to comprehensively evaluate IoT system security. It builds a multi-layer IoT hypothesis graph by simultaneously modeling all of the essential components in IoT systems, including the physical environment, devices, communication protocols, and applications. The model checker can then analyze the generated hypothesis graph to validate system security properties or generate attack paths if there are any violations. An optimization algorithm is further introduced to reduce the computational complexity of our analysis. Our framework verifies hypothesis graphs with millions of nodes in less than 100 seconds. The illustrative case studies show that our framework can detect more potential threats than the existing approaches.