Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTiramisu: Fast and General Network Verification
65
0
0.0
(
0
)
Added by
Anubhavnidhi Abhashkumar
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Todays distributed network control planes support multiple routing protocols, filtering mechanisms, and route selection policies. These protocols operate at different layers, e.g. BGP operates at the EGP layer, OSPF at the IGP layer, and VLANs at layer 2. The behavior of a networks control plane depends on how these protocols interact with each other. This makes network configurations highly complex and error-prone. State-of-the-art control plane verifiers are either too slow, or do not model certain features of the network. In this paper, we propose a new multilayer hedge graph abstraction, Tiramisu, that supports fast verification of the control plane. Tiramisu uses a combination of graph traversal algorithms and ILPs (Integer Linear Programs) to check different network policies. We use Tiramisu to verify policies of various real-world and synthetic configurations. Our experiments show that Tiramisu can verify any policy in < 0.08 s in small networks (~35 devices) and < 0.12 s in large networks (~160 devices), and it is 10-600X faster than state-of-the-art without losing generality.
rate research
Read More
Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC). Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead. However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNFs set of PECs is not minimal. We show that ddNFs non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification. Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, #PEC, that advances the field as follows: (i) #PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) #PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, #PEC is 10X faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.
To use neural networks in safety-critical settings it is paramount to provide assurances on their runtime operation. Recent work on ReLU networks has sought to verify whether inputs belonging to a bounded box can ever yield some undesirable output. Input-splitting procedures, a particular type of verification mechanism, do so by recursively partitioning the input set into smaller sets. The efficiency of these methods is largely determined by the number of splits the box must undergo before the property can be verified. In this work, we propose a new technique based on shadow prices that fully exploits the information of the problem yielding a more efficient generation of splits than the state-of-the-art. Results on the Airborne Collision Avoidance System (ACAS) benchmark verification tasks show a considerable reduction in the partitions generated which substantially reduces computation times. These results open the door to improved verification methods for a wide variety of machine learning applications including vision and control.
It has been recently brought into spotlight that through the exploitation of network coding concepts at physical-layer, the interference property of the wireless media can be proven to be a blessing in disguise. Nonetheless, most of the previous studies on this subject have either held unrealistic assumptions about the network properties, thus making them basically theoretical, or have otherwise been limited to fairly simple network topologies. We, on the other hand, believe to have devised a novel scheme, called Real Amplitude Scaling (RAS), that relaxes the aforementioned restrictions, and works with a wider range of network topologies and in circumstances that are closer to practice, for instance in lack of symbol-level synchronization and in the presence of noise, channel distortion and severe interference from other sources. The simulation results confirmed the superior performance of the proposed method in low SNRs, as well as the high SNR limits, where the effect of quantization error in the digital techniques becomes comparable to the channel.
Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to observe the PSN in a generic 2x2 mesh NoC with a uniform random traffic load. Key features of PSN are measured at the behavioral level. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.
We consider the problem of distributed scheduling in wireless networks where heterogeneously delayed information about queue lengths and channel states of all links are available at all the transmitters. In an earlier work (by Reddy et al. in Queueing Systems, 2012), a throughput optimal scheduling policy (which we refer to henceforth as the R policy) for this setting was proposed. We study the R policy, and examine its two drawbacks -- (i) its huge computational complexity, and (ii) its non-optimal average per-packet queueing delay. We show that the R policy unnecessarily constrains itself to work with information that is more delayed than that afforded by the system. We propose a new policy that fully exploits the commonly available information, thereby greatly improving upon the computational complexity and the delay performance of the R policy. We show that our policy is throughput optimal. Our main contribution in this work is the design of two fast and near-throughput-optimal policies for this setting, whose explicit throughput and runtime performances we characterize analytically. While the R policy takes a few milliseconds to several tens of seconds to compute the schedule once (for varying number of links in the network), the running times of the proposed near-throughput-optimal algorithms range from a few microseconds to only a few hundred microseconds, and are thus suitable for practical implementation in networks with heterogeneously delayed information.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
