Recent trends in software-defined networking have extended network programmability to the data plane. Unfortunately, the chance of introducing bugs increases significantly. Verification can help prevent bugs by assuring that the program does not violate its requirements. Although research on the verification of P4 programs is very active, we still need tools to make easier for programmers to express properties and to rapidly verify complex invariants. In this paper, we leverage assertions and symbolic execution to propose a more general P4 verification approach. Developers annotate P4 programs with assertions expressing general network correctness properties; the result is transformed into C models and all possible paths symbolically executed. We implement a prototype, and use it to show the feasibility of the verification approach. Because symbolic execution does not scale well, we investigate a set of techniques to speed up the process for the specific case of P4 programs. We use the prototype implemented to show the gains provided by three speed up techniques (use of constraints, program slicing, parallelization), and experiment with different compiler optimization choices. We show our tool can uncover a broad range of bugs, and can do it in less than a minute considering various P4 applications.
more »
« less
P4BID: information flow control in p4
Modern programmable network switches can implement cus-
tom applications using efficient packet processing hardware,
and the programming language P4 provides high-level con-
structs to program such switches. The increase in speed and
programmability has inspired research in dataplane program-
ming, where many complex functionalities, e.g., key-value
stores and load balancers, can be implemented entirely in
network switches. However, dataplane programs may suffer
from novel security errors that are not traditionally found
in network switches.
To address this issue, we present a new information-flow
control type system for P4. We formalize our type system in a
recently-proposed core version of P4, and we prove a sound-
ness theorem: well-typed programs satisfy non-interference.
We also implement our type system in a tool, P4BID, which
extends the type checker in the p4c compiler, the reference
compiler for the latest version of P4. We present several case
studies showing that natural security, integrity, and isolation
properties in networks can be captured by non-interference,
and our type system can detect violations of these properties
while certifying correct programs.
more »
« less
- NSF-PAR ID:
- 10341748
- Date Published:
- Journal Name:
- PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
- Page Range / eLocation ID:
- 46 to 60
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.more » « less
-
We present Contra, a system for performance-aware routing that can adapt to traffic changes at hardware speeds. While point solutions exist for a fixed topology (e.g., a Fattree) with a fixed routing policy (e.g., use least utilized paths), Contra can operate seamlessly over any network topology and a wide variety of sophisticated routing policies. Users of Contra write network-wide policies that rank network paths given their current performance. A compiler then analyzes such policies in conjunction with the network topology and decomposes them into switch-local P4 programs, which collectively implement a new, specialized distance-vector protocol. This protocol generates compact probes that traverse the network, gathering path metrics to optimize for the user policy dynamically. Switches respond to changing network conditions by routing flowlets along the best policy-compliant paths. Our experiments show that Contra scales to large networks, and that in terms of flow completion times, it is competitive with hand-crafted systems that have been customized for specific topologies and policies.more » « less
-
P4 (Programming Protocol-Independent Packet Processors) represents a paradigm shift in network programmability by providing a high-level language to define packet processing behavior in network switches/devices. The importance of P4 lies in its ability to overcome the limitations of OpenFlow, the previous de facto standard for software-defined networking (SDN). Unlike OpenFlow, which operates on fixed match-action tables, P4 offers an approach where network operators can define packet processing behaviors at various protocol layers. P4 provides a programmable platform to create and implement custom network switches/devices protocols. However, this opens a new attack surface for threat actors who can access P4-enabled switches/devices and manipulate custom protocols for malicious purposes. Attackers can craft malicious packets to exploit protocol-specific vulnerabilities in these network devices. This ongoing research work proposes a blockchain-based model to secure P4 custom protocols. The model leverages the blockchain’s immutability, tamperproof ability, distributed consensus for protocol governance, and auditing to guarantee the transparency, security, and integrity of custom protocols defined in P4 programmable switches. The protocols are recorded as transactions and stored on the blockchain network. The model's performance will be evaluated using execution time in overhead computation, false positive rate, and network scalability.more » « less
-
One of the main roles of the Domain Name System (DNS) is to map domain names to IP addresses. Despite the importance of this function, DNS traffic often passes without being analyzed, thus making the DNS a center of attacks that keep evolving and growing. Software-based mitigation approaches and dedicated state-of-the-art firewalls can become a bottleneck and are subject to saturation attacks, especially in high-speed networks. The emerging P4-programmable data plane can implement a variety of network security mitigation approaches at high-speed rates without disrupting legitimate traffic. This paper describes a system that relies on programmable switches and their stateful processing capabilities to parse and analyze DNS traffic solely in the data plane, and subsequently apply security policies on domains according to the network administrator. In particular, Deep Packet Inspection (DPI) is leveraged to extract the domain name consisting of any number of labels and hence, apply filtering rules (e.g., blocking malicious domains). Evaluation results show that the proposed approach can parse more domain labels than any state-of-the-art P4-based approach. Additionally, a significant performance gain is attained when comparing it to a traditional software firewall -pfsense-, in terms of throughput, delay, and packet loss. The resources occupied by the implemented P4 program are minimal, which allows for more security functionalities to be added.more » « less