To address spatial imbalances in the supply and demand of drivers, ridesharing platforms can make use of policies to direct driver relocation. We study a simple model of this problem, which allows us to give a constructive characterization of the unique fixpoint of system dynamics. Using this construction, we design a dynamic policy that provides stronger, than previous work, guarantees about its rate of convergence to the fixpoint. Simulations demonstrate the benefits of our approach.

QUIC is a new Internet secure transport protocol currently in the process of IETF standardization. It is intended as a replacement for the TLS/TCP stack and will be the basis of HTTP/3, the next official version of the hypertext transfer protocol. As a result, it is likely, in the near future, to carry a substantial fraction of traffic on the Internet. We describe our experience applying a methodology of compositional specification-based testing to QUIC. We develop a formal specification of the wire protocol, and use this specification to generate automated randomized testers for implementations of QUIC. The testers effectively take one role of the QUIC protocol, interacting with the other role to generate full protocol executions, and verifying that the implementations conform to the formal specification. This form of testing generates significantly more diverse stimuli and stronger correctness criteria than interoperability testing, the primary method used to date to validate QUIC and its implementations. As a result, numerous implementation errors have been found. These include some vulnerabilities at the protocol and implementation levels, such as an off-path denial of service scenario and an information leak similar to the "heartbleed" vulnerability in OpenSSL.

Memory errors such as buffer overruns are notorious security vulnerabilities. There has been considerable interest in having a compiler to ensure the safety of compiled code either through static verification or through instrumented runtime checks. While certifying compilation has shown much promise, it has not been practical, leaving code instrumentation as the next best strategy for compilation. We term such compilers Memory Error Sanitization Compilers (MESCs). MESCs are available as part of GCC, LLVM and MSVC suites. Due to practical limitations, MESCs typically apply instrumentation indiscriminately to every memory access, and are consequently prohibitively expensive and practical to only small code bases. This work proposes a methodology that applies state-of-the-art static analysis techniques to eliminate unnecessary runtime checks, resulting in more efficient and scalable defenses. The methodology was implemented on LLVM's Safecode, Integer Overflow, and Address Sanitizer passes, using static analysis of Frama-C and Codesurfer. The benchmarks demonstrate an improvement in runtime performance that makes incorporation of runtime checks a viable option for defenses.

Parameter tampering attacks are dangerous to a web application whose server performs weaker data sanitization than its client. This paper presents TamperProof, a methodology and tool that offers a novel and efficient mechanism to protect Web applications from parameter tampering attacks. TamperProof is an online defense deployed in a trusted environment between the client and server and requires no access to, or knowledge of, the server side codebase, making it effective for both new and legacy applications. The paper reports on experiments that demonstrate TamperProof's power in efficiently preventing all known parameter tampering vulnerabilities on ten different applications.

Access control schemes come in all shapes and sizes, which makes choosing the right one for a particular application a challenge. Yet today's techniques for comparing access control schemes completely ignore the setting in which the scheme is to be deployed. In this paper, we present a formal framework for comparing access control schemes with respect to a particular application. The analyst's main task is to evaluate an access control scheme in terms of how well it implements a given access control workload (a formalism that we introduce to represent an application's access control needs). One implementation is better than another if it has stronger security guarantees, and in this paper we introduce several such guarantees: correctness, homomorphism, AC-preservation, safety, administration-preservation, and compatibility. The scheme that admits the implementation with the strongest guarantees is deemed the best fit for the application. We demonstrate the use of our framework by evaluating two workloads on ten different access control schemes.

LambdaRAM is a high-performance, multidimensional, wide-area, distributed cache that takes advantage of massively available memory from multiple clusters interconnected by ultra high-speed networking to provide data-intensive scientific applications with rapid access to both local and remote data without suffering the latency bottlenecks often associated with large storage systems and wide-area data access. LambdaRAM has been demonstrated to yield significant performance speed-ups for geophysical and Bioscience applications accessing extremely large datasets. Currently, LambdaRAM is being integrated by NASA for the modelling, analysis and prediction (MAP) program applications to study tropical cyclones. Formal verification o/LambdaRAM is important to NASA to ensure that LambdaRAM operates reliably in real-time mission critical deployments. We present our preliminary steps towards full formal verification of LambdaRAM. We first give an abstract description of the system and then verify several of its properties. Most of the proofs are accomplished by automatic techniques, while some require deductive steps.

We show how to verify the correctness of transactional memory implementations with a model checker. We show how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies this specification. This notion of an admissible interchange is a key to our ability to use a model checker, and lets us capture the various notions of transaction conflict as characterized by Scott. We demonstrate our work using the TLC model checker to verify several well-known implementations described abstractly in the TLA+ specification language.

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication. In this paper we show how the Dolev–Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We illustrate this method where the cryptographic primitives are based on Carter–Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds.

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication.In this paper we show how the Dolev-Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We develop this method where the cryptographic primitives are based on Carter-Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds.

: We describe a fault-tolerant distributed storage system for local area networks. Our system implements Persistent, Associative, Shared Object (PASO) memory. A PASO memory stores a set of data objects that can be accessed by associative search queries from all nodes in an ensemble of machines. This approach to distributed memory has been used in a number of systems, and provides a convenient and useful model for parallel and distributed applications. PASO memory is amenable to adaptive implementations that relocate data objects in response to changing network configurations and access patterns, making it a good candidate for an efficient, fault-tolerant storage system. The paper defines the semantics of PASO memory, gives a basic design strategy, discusses memory primitives and their costs, and discusses adaptive techniques for improving efficiency. 1 Introduction This paper presents PASO, a Persistent, Associative, Shared Object memory, and studies algorithms that implement fault-t...

Layered communicationprotocols frequently implement a FIFO message fiacility cm top of an unrehable non-FIFO serwce such as that provided hy a packet-swltchmg network.This paper investigates the possibdity of Implementing a reliable message layer on top of an underlying layer that can low packets and deliver them out of order, with the addltlonzd restriction that the implementatmn uses only a fixed fimte number of different packets.A new formalism is presented to spcclfy communication layers and their properties, the notion of their implementation by 1/0 automata.and the properties of such implementations.An 1/0 automaton that Implements a rellable layer over an unreliable layer is presented In this implementation, tbe number ot packets needed to deliver each succeeding message increases permanently as additional packet-loss and reordering faults occur.A proof is gwen that no protocol can avoid such performance degradatmn.

Two-way translations between various versions of temporal logic and between temporal logic over finite sequences and star-free regular expressions are presented. The main result is a translation from normal-form temporal logic formulas to formulas that use only future operators. The translation offers a new proof to a theorem claimed by D. Gabbay et al. (1980), stating that restricting temporal logic to the future operators does not impair its expressive power. The theorem is the basis of many temporal proof systems.>

A high-level, knowledge-based approach for deriving a family of protocols for thesequence transmissionproblem is presented. The protocols of Aho et al. [2, 3], the Alternating Bit protocol [5], and Stenning's protocol [44] are all instances of one knowledge-based protocol that is derived. The derivation in this paper leads to transparent and uniform correctness proofs for all these protocols.

Article Free Access Share on Real-time sequence transmission problem Authors: Da-Wei Wang Department of Computer Science, Yale University, New Haven, CT Department of Computer Science, Yale University, New Haven, CTView Profile , Lenore Zuck Department of Computer Science, Yale University, New Haven, CT Department of Computer Science, Yale University, New Haven, CTView Profile Authors Info & Claims PODC '91: Proceedings of the tenth annual ACM symposium on Principles of distributed computingJuly 1991 Pages 111–123https://doi.org/10.1145/112600.112611Published:01 July 1991Publication History 4citation217DownloadsMetricsTotal Citations4Total Downloads217Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

We investigate the problem of transmitting sequences over unreliable channels where both the data items and the message alphabet have finite domains.We show tight bounds on the number of different sequences that can be transmitted (as a function of size of the message alphabet) when the channel can (1) reorder and duplicate messages and (2) reorder and delete messages.All of our results are derived using formal reasoning about, knowledge.

A new probabilistic symmetric solution to the n processes mutual exclusion problem is presented. The algorithm is verified formally using the extreme fairness approach to probabilistic verification.