- Award ID(s):
- 2123864
- PAR ID:
- 10533353
- Publisher / Repository:
- ACM
- Date Published:
- ISBN:
- 9798400702297
- Page Range / eLocation ID:
- 113 to 129
- Format(s):
- Medium: X
- Location:
- Koblenz Germany
- Sponsoring Org:
- National Science Foundation
More Like this
-
This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework's proofs are machine checked.more » « less
-
mmWave communication has been recognized as a highly promising technology for 5G wireless backhaul, which is capable of providing multi-gigabit per second transmission rates. However, in urban wireless backhaul environments, unforeseen events can cause short-term blockages or node failures and, therefore, network survivability is extremely important. In this paper, we investigate a novel relay-assisted mmWave backhaul network architecture, where a number of small-cell BSs and relays are deployed, e.g. on the lampposts of urban streets. Relays are used to provide multi-hop line-of-sight paths between small-cell BSs, which form logical links of the network. In this scenario, the interconnected logical links make up a mesh network, which offers opportunities for both link-level and network-level reconfiguration. We propose two joint link-network level reconfiguration schemes for recovery after exceptional events. One prioritizes relay path (link-level) reconfiguration and uses alternate network-level paths only if necessary. The other splits traffic on both reconfigured links and backup paths to improve network throughput. Simulation results demonstrate that the proposed schemes significantly outperform purely link-level and purely network-level reconfiguration schemes. The proposed approaches are shown to not only maintain high network throughput but to also provide robust blockage/fault tolerance across a range of scenarios for urban mmWave backhaul networks.more » « less
-
This paper introduces sharable backup as a novel solution to failure recovery in data center networks. It allows the entire network to share a small pool of backup devices. This proposal is grounded in three key observations. First, the traditional rerouting-based failure recovery is ineffective, because bandwidth loss from failures degrades application performance drastically. Therefore, failed devices should be replaced to restore bandwidth. Second, failures in data centers are rare but destructive [11], so it is desirable to seek cost-effective backup options. Third, the emergence of configurable data center network architectures promises feasibility of bringing backup devices online dynamically. We design the ShareBackup prototype architecture to realize this idea. Compared to rerouting-based solutions, ShareBackup provides more bandwidth with short path length at low cost.more » « less
-
Reasoning about storage systems is challenging because these systems make persistence guarantees even if the system crashes at any point. To achieve these crash-safety guarantees, storage systems include recovery procedures to restore the system to a consistent state after a crash. Moreover, large-scale systems are structured as multiple stacked layers and can require recovery at multiple layers of abstraction. Formal verification can ensure that crash-safety guarantees hold regardless of when the system crashes. To make verification tractable, large-scale systems should be verified in a modular fashion, layer-by-layer in the software stack. Layered recovery makes modularity challenging because the system can crash in the middle of a high-level recovery procedure and must start over from the low-level recovery procedure. We present Argosy, a framework for machine-checked proofs of storage systems that supports layered recovery implementations with modular proofs. The framework is based on combinators for transition relations that are inspired by Kleene algebra, which provides a convenient formalism for specifying and reasoning about crashes and recovery. On top of this framework, we implement Crash Hoare Logic (CHL), the program logic used by FSCQ. Using the logic, we have verified an example of layered recovery featuring a write-ahead log on top of a disk, which itself runs by replicating over two unreliable disks. The metatheory of the framework, the soundness of the program logic, and these examples are all verified in the Coq theorem prover.more » « less
-
In this paper, we present a game-theoretic analysis of ransomware. To this end, we provide theoretical and empirical analysis of a two-player Attacker-Defender (A-D) game, as well as a Defender-Insurer (D-I) game; in the latter, the attacker is assumed to be a non-strategic third party. Our model assumes that the defender can invest in two types of protection against ransomware attacks: (1) general protection through a deterrence effort, making attacks less likely to succeed, and (2) a backup effort serving the purpose of recourse, allowing the defender to recover from successful attacks. The attacker then decides on a ransom amount in the event of a successful attack, with the defender choosing to pay ransom immediately, or to try to recover their data first while bearing a recovery cost for this recovery attempt. Note that recovery is not guaranteed to be successful, which may eventually lead to the defender paying the demanded ransom. Our analysis of the A-D game shows that the equilibrium falls into one of three scenarios: (1) the defender will pay the ransom immediately without having invested any effort in backup, (2) the defender will pay the ransom while leveraging backups as a credible threat to force a lower ransom demand, and (3) the defender will try to recover data, only paying the ransom when recovery fails. We observe that the backup effort will be entirely abandoned when recovery is too expensive, leading to the (worst-case) first scenario which rules out recovery. Furthermore, our analysis of the D-I game suggests that the introduction of insurance leads to moral hazard as expected, with the defender reducing their efforts; less obvious is the interesting observation that this reduction is mostly in their backup effort.