In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus, effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this article, we investigate the alternative semantics for ATL*where the past is not forgotten in nested games. We show that the standard semantics of ATL*coincides with the “truly perfect recall” semantics for agents with perfect information and in case of so-called “objective” abilities under uncertainty. On the other hand, the two semantics differ significantly for the most popular (“subjective”) notion of ability under imperfect information. The same applies to the standard vs. “truly perfect recall” semantics of ATL*with persistent strategies. We compare the relevant variants of ATL*by looking at their expressive power, sets of validities, and tractability of model checking.

We present Vera, a tool that verifies P4 programs using symbolic execution. Vera automatically uncovers a number of common bugs including parsing/deparsing errors, invalid memory accesses, loops and tunneling errors, among others. Vera can also be used to verify user-specified properties in a novel language we call NetCTL. To enable scalable, exhaustive verification of P4 program snapshots, Vera automatically generates all valid header layouts and uses a novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes between 5s-15s to track the execution of a purely symbolic packet in the largest P4 program currently available (6KLOC) and can compute SEFL model updates in milliseconds. Vera can also explore multiple concrete dataplanes at once by allowing the programmer to insert symbolic table entries; the resulting verification highlights possible control plane errors. We have used Vera to analyze many P4 programs including the P4 tutorials, P4 programs in the research literature and the switch code from https://p4.org. Vera has found several bugs in each of them in seconds/minutes.

Multipath congestion control prefers sending more traffic over paths with lower loss rates. This behaviour is key to achieving resource pooling and efficiently allocating resources in multipath networks. However, loss rates can be manipulated in the Internet by service providers to trick multipath traffic to travel via different paths. We show how providers can use policy drop to artificially increase the loss rate for all traffic using information about client subscriptions (i.e. speed of access links) and per-connection RTTs such that regular TCP throughput is unaffected, and Multipath TCP traffic is rerouted to other paths when alternatives exist. Policy drop is cheap: our prototype does not hold per flow state and can process in excess of 64B 9Mbps on a single machine, or 40Gbps with Internet-sized packets. Finally, we use game theory to understand the implications of policy drop on the Internet ecosystem. Our results show that policy drop will be widely deployed for low-bandwidth subscriptions, and may be deployed for higher-throughput subscriptions too.

We present SymNet, a network static analysis tool based on symbolic execution. SymNet injects symbolic packets and tracks their evolution through the network. Our key novelty is SEFL, a language we designed for expressing data plane processing in a symbolic-execution friendly manner. SymNet statically analyzes an abstract data plane model that consists of the SEFL code for every node and the links between nodes. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while verifying packet header memory-safety and covering network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug mid- dlebox interactions from the literature, to check properties of our department’s network and the Stanford backbone. Modeling network functionality is not easy. To aid users we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configura- tions and arbitrary Click modular router configurations. The parsers rely on prebuilt models that are exact and fast to an- alyze. Finally, we have built an automated testing tool that combines symbolic execution and testing to check whether the model is an accurate representation of the real code.

Network Function Virtualization is pushing network operators to deploy commodity hardware that will be used to run middlebox functionality and processing on behalf of third parties: in effect, network operators are slowly but surely becoming in-network cloud providers. The market for innetwork clouds is large, ranging from content providers, mobile applications and even end-users.

Mobile ad hoc networks are networks that allow (mobile) users to communicate in heterogeneous environments without relying on a fixed infrastructure, examples of which are mobile communication in large urban spaces or in public transportation. Due to their many advantages, such as decentralization, independence of communication infrastructure, flexibility etc., their field of use steadily increases. However, networks of this kind also raise new problems related to, for example, routing and data delivery, security and privacy, trust and usability. In this article, we propose a formal model of mobile ad hoc networks and address questions regarding optimal and stable network topologies. In particular, stability is important to ensure that communication is reliable and that applications designed for such networks are accepted by the users. We analyse stability from a game theoretic point of view, and propose a non-cooperative as well as a cooperative modelling. Moreover, we allow users to express constraints on how their communication should be handled in the network in order to ensure user constraints, e.g. related to privacy and security. For this purpose we use the temporal logic CTL. Finally, we analyse the complexity of associated verification and synthesis problems regarding optimal/stable network topologies.

In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past.

In order to improve users ability to interact with devices in an intelligent house, we propose a platform for intelligent device composition, based on Service Oriented Architecture. In such an environment, devices can be controlled and monitored using Service invocations, or they can interoperate in order to fulfil complex tasks, using Service composition. As part of our platform, we define a language for dynamic service composition, called MetaBPEL. It extends the WS-BPEL 2.0 language with semantic information, and acts as an abstract workflow definition mechanism. Unlike BPEL and other conventional composition languages, MetaBPEL does not bind to actual service implementations, but merely describes capabilities that services must have, in order to participate in a workflow. This feature allows both workflow migration between different environments as well as service replacement without modifying the composition scheme. In the article, we describe the MetaBPEL structure and the associated creation, generalization and instantiation mechanisms.