اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدFormally Verified Convergence of Policy-Rich DBF Routing Protocols
71
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In this paper we present new general convergence results about the behaviour of Distributed Bellman-Ford (DBF) family of routing protocols, which includes distance-vector protocols (e.g. RIP) and path-vector protocols (e.g. BGP). First, we propose a new algebraic model for abstract routing problems which has fewer primitives than previous models and can represent more expressive policy languages. The new model is also the first to allow concurrent reasoning about distance-vector and path-vector protocols. Second, we explicitly demonstrate how DBF routing protocols are instances of a larger class of asynchronous iterative algorithms, for which there already exist powerful results about convergence. These results allow us to build upon conditions previously shown by Sobrinho to be sufficient and necessary for the convergence of path-vector protocols and generalise and strengthen them in various ways: we show that, with a minor modification, they also apply to distance-vector protocols; we prove they guarantee that the final routing solution reached is unique, thereby eliminating the possibility of anomalies such as BGP wedgies; we relax the model of asynchronous communication, showing that the results still hold if routing messages can be lost, reordered, and duplicated. Thirdly, our model and our accompanying theoretical results have been fully formalised in the Agda theorem prover. The resulting library is a powerful tool for quickly prototyping and formally verifying new policy languages. As an example, we formally verify the correctness of a policy language with many of the features of BGP including communities, conditional policy, path-inflation and route filtering.
قيم البحث
اقرأ أيضاً
Reactive routing protocols are gaining popularity due to their event driven nature day by day. In this vary paper, reactive routing is studied precisely. Route request, route reply and route maintenance phases are modeled with respect to control over
head. Control overhead varies with respect to change in various parameters. Our model calculates these variations as well. Besides modeling, we chose three most favored reactive routing protocols as Ad-Hoc on Demand Distance Vector (AODV), Dynamic Source Routing (DSR) and Dynamic MANET on Demand (DYMO) for our experiments. We simulated these protocols using ns-2 for a detailed comparison and performance analysis with respect to mobility and scalability issues keeping metrics of throughput, route delay and control over head. Their performances and comparisons are extensively presented in last part of our work.
To ensure seamless communication in wireless multi-hop networks, certain classes of routing protocols are defined. This vary paper, is based upon proactive routing protocols for Wireless multihop networks. Initially, we discuss Destination Sequence D
istance Vector (DSDV), Fish-eye State Routing (FSR) and Optimized Link State Routing (OLSR), precisely followed by mathematical frame work of control overhead regarding proactive natured routing protocols. Finally, extensive simulations are done using NS 2 respecting above mentioned routing protocols covering mobility and scalability issues. Said protocols are compared under mobile and dense environments to conclude our performance analysis.
An attacker that gains access to a cryptocurrency users private keys can perform any operation in her stead. Due to the decentralized nature of most cryptocurrencies, no entity can revert those operations. This is a central challenge for decentralize
d systems, illustrated by numerous high-profile heists. Vault contracts reduce this risk by introducing artificial delay on operations, allowing abortion by the contract owner during the delay. However, the theft of a key still renders the vault unusable and puts funds at risk. We introduce Phoenix, a novel contract architecture that allows the user to restore its security properties after key loss. Phoenix takes advantage of users ability to store keys in easily-available but less secure storage (tier-two) as well as more secure storage that is harder to access (tier-one). Unlike previous solutions, the user can restore Phoenix security after the theft of tier-two keys and does not lose funds despite losing keys in either tier. Phoenix also introduces a mechanism to reduce the damage an attacker can cause in case of a tier-one compromise. We formally specify Phoenixs required behavior and provide a prototype implementation of Phoenix as an Ethereum contract. Since such an implementation is highly sensitive and vulnerable to subtle bugs, we apply a formal verification tool to prove specific code properties and identify faults. We highlight a bug identified by the tool that could be exploited by an attacker to compromise Phoenix. After fixing the bug, the tool proved the low-level executable codes correctness.
Routing plays a fundamental role in network applications, but it is especially challenging in Delay Tolerant Networks (DTNs). These are a kind of mobile ad hoc networks made of e.g. (possibly, unmanned) vehicles and humans where, despite a lack of co
ntinuous connectivity, data must be transmitted while the network conditions change due to the nodes mobility. In these contexts, routing is NP-hard and is usually solved by heuristic store and forward replication-based approaches, where multiple copies of the same message are moved and stored across nodes in the hope that at least one will reach its destination. Still, the existing routing protocols produce relatively low delivery probabilities. Here, we genetically improve two routing protocols widely adopted in DTNs, namely Epidemic and PRoPHET, in the attempt to optimize their delivery probability. First, we dissect them into their fundamental components, i.e., functionalities such as checking if a node can transfer data, or sending messages to all connections. Then, we apply Genetic Improvement (GI) to manipulate these components as terminal nodes of evolving trees. We apply this methodology, in silico, to six test cases of urban networks made of hundreds of nodes, and find that GI produces consistent gains in delivery probability in four cases. We then verify if this improvement entails a worsening of other relevant network metrics, such as latency and buffer time. Finally, we compare the logics of the best evolved protocols with those of the baseline protocols, and we discuss the generalizability of the results across test cases.
We present Revel, a partially neural reinforcement learning (RL) framework for provably safe exploration in continuous state and action spaces. A key challenge for provably safe deep RL is that repeatedly verifying neural networks within a learning l
oop is computationally infeasible. We address this challenge using two policy classes: a general, neurosymbolic class with approximate gradients and a more restricted class of symbolic policies that allows efficient verification. Our learning algorithm is a mirror descent over policies: in each iteration, it safely lifts a symbolic policy into the neurosymbolic space, performs safe gradient updates to the resulting policy, and projects the updated policy into the safe symbolic subset, all without requiring explicit verification of neural networks. Our empirical results show that Revel enforces safe exploration in many scenarios in which Constrained Policy Optimization does not, and that it can discover policies that outperform those learned through prior approaches to verified exploration.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
