Biblio

We develop a theory of inductive and coinductive session types in a computational interpretation of linear logic, enabling the representation of potentially infinite interactions in a compositionally sound way that preserves logical soundness, a major stepping stone towards a full dependent type theory for expressing and reasoning about session-based concurrent higher order distributed programs. The language consists of a λ-calculus with inductive types and a contextual monadic type encapsulating session-based concurrency, treating monadic values as first-class objects. We consider general fixpoint and cofixpoint constructs, subject to natural syntactic constraints, as a means of producing inductive and coinductive definitions of session-typed processes, that until now have only been considered using general recursion, which is incompatible with logical consistency and introduces compositional divergence. We establish a type safety result for our language, including protocol compliance and progress of concurrent computation, and also show, through a logical relations argument, that all well-typed programs are compositionally non-divergent. Our results entail the logical soundness of the framework, and enable compositional reasoning about useful infinite interactive behaviors, while ruling out unproductive infinite behavior.

Software services and governing communication protocols are increasingly domain-aware. Domains can have multiple interpretations, such as the principals on whose behalf processes act or the location at which parties reside. Domains impact protocol compliance and access control, two central issues to overall functionality and correctness in distributed systems. This paper proposes a session-typed process framework for domain-aware communication-centric systems based on a CurryHoward interpretation of linear logic, here augmented with nominals from hybrid logic indicating domains. These nominals are explicit in the process expressions and govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics for modal logic. Flexible access relationships among domains can be elegantly defined and statically enforced. The framework can also account for scenarios in which domain information is discovered only at runtime. Due to the logical origins of our systems, well-typed processes enjoy session fidelity, global progress, and termination. Moreover, well-typed processes always respect the accessibility relation and satisfy a form of domain parametricity, two properties crucial to show that domain-related properties of concrete programs are satisfied. 

This paper describes the development of subsymbolic ACT-R models for the Concentration game. Performance data is taken from an experiment in which participants played the game un- der two conditions: minimizing the number of mismatches/ turns during a game, and minimizing the time to complete a game. Conflict resolution and parameter tuning are used to implement an accuracy model and a speed model that capture the differences for the two conditions. Visual attention drives exploration of the game board in the models. Modeling re- sults are generally consistent with human performance, though some systematic differences can be seen. Modeling decisions, model limitations, and open issues are discussed. 

We introduce a framework for controlling the energy provided or absorbed by distributed energy resources (DERs) in power distribution networks. In this framework, there is a set of agents referred to as aggregators that interact with the wholesale electricity market, and through some market-clearing mechanism, are requested (and will be compensated for) to provide (or absorb) certain amount of active (or reactive) power over some period of time. In order to fulfill the request, each aggregator interacts with a set of DERs and offers them some price per unit of active (or reactive) power they provide (or absorb); the objective is for the aggregator to design a pricing strategy for incentivizing DERs to change its active (or reactive) power consumption (or production) so as they collectively provide the amount that the aggregator has been asked for. In order to make a decision, each DER uses the price information provided by the aggregator and some estimate of the average active (or reactive) power that neighboring DERs can provide computed through some exchange of information among them; this exchange is described by a connected undirected graph. The focus is on the DER strategic decision-making process, which we cast as a game. In this context, we provide sufficient conditions on the aggregator's pricing strategy under which this game has a unique Nash equilibrium. Then, we propose a distributed iterative algorithm that adheres to the graph that describes the exchange of information between DERs that allows them to seek for this Nash equilibrium. We illustrate our results through several numerical simulations.

As designers conceive and implement what are commonly (but mistakenly) called autonomous systems, they adhere to certain myths of autonomy that are not only damaging in their own right, but also by their continued propagation. This article busts such myths and gives reasons why each of these myths should be called out and cast aside.

The goal of this roadmap paper is to summarize the stateof-the-art and identify research challenges when developing, deploying and managing self-adaptive software systems. Instead of dealing with a wide range of topics associated with the field, we focus on four essential topics of self-adaptation: design space for self-adaptive solutions, software engineering processes for self-adaptive systems, from centralized to decentralized control, and practical run-time verification & validation for self-adaptive systems. For each topic, we present an overview, suggest future directions, and focus on selected challenges. This paper complements and extends a previous roadmap on software engineering for self-adaptive systems published in 2009 covering a different set of topics, and reflecting in part on the previous paper. This roadmap is one of the many results of the Dagstuhl Seminar 10431 on Software Engineering for Self-Adaptive Systems, which took place in October 2010.

The simplest and purest practical object-oriented language designs
today are seen in dynamically-typed languages, such as Smalltalk
and Self. Static types, however, have potential benefits for productivity,
security, and reasoning about programs. In this paper, we describe
the design of Wyvern, a statically typed, pure object-oriented
language that attempts to retain much of the simplicity and expressiveness
of these iconic designs.
Our goals lead us to combine pure object-oriented and functional
abstractions in a simple, typed setting. We present a foundational
object-based language that we believe to be as close as
one can get to simple typed lambda calculus while keeping objectorientation.
We show how this foundational language can be translated
to the typed lambda calculus via standard encodings. We then
define a simple extension to this language that introduces classes
and show that classes are no more than sugar for the foundational
object-based language. Our future intention is to demonstrate that
modules and other object-oriented features can be added to our language
as not more than such syntactical extensions while keeping
the object-oriented core as pure as possible.
The design of Wyvern closely follows both historical and modern
ideas about the essence of object-orientation, suggesting a new
way to think about a minimal, practical, typed core language for
objects.

In prior research we have developed a Curry-Howard interpretation of linear sequent calculus as session-typed processes. In this paper we uniformly integrate this computational interpretation in a functional language via a linear contextual monad that isolates session-based concurrency. Monadic values are open process expressions and are first class objects in the language, thus providing a logical foundation for higher-order session typed processes. We illustrate how the combined use of the monad and recursive types allows us to cleanly write a rich variety of concurrent programs, including higher-order programs that communicate processes. We show the standard metatheoretic result of type preservation, as well as a global progress theorem, which to the best of our knowledge, is new in the higher-order session typed setting.

Self-diagnosis is a fundamental capability of self-adaptive systems. In order to recover from faults, systems need to know which part is responsible for the incorrect behavior. In previous work we showed how to apply a design-time diagnosis technique at run time to identify faults at the architectural level of a system. Our contributions address three major shortcomings of our previous work: 1) we present an expressive, hierarchical language to describe system behavior that can be used to diagnose when a system is behaving different to expectation; the hierarchical language facilitates mapping low level system events to architecture level events; 2) we provide an automatic way to determine how much data to collect before an accurate diagnosis can be produced; and 3) we develop a technique that allows the detection of correlated faults between components. Our results are validated experimentally by injecting several failures in a system and accurately diagnosing them using our algorithm.

Since conventional software security approaches are often manually developed and statically deployed, they are no longer sufficient against today's sophisticated and evolving cyber security threats. This has motivated the development of self-protecting software that is capable of detecting security threats and mitigating them through runtime adaptation techniques. In this paper, we argue for an architecture-based self- protection (ABSP) approach to address this challenge. In ABSP, detection and mitigation of security threats are informed by an architectural representation of the running system, maintained at runtime. With this approach, it is possible to reason about the impact of a potential security breach on the system, assess the overall security posture of the system, and achieve defense in depth. To illustrate the effectiveness of this approach, we present several architecture adaptation patterns that provide reusable detection and mitigation strategies against well-known web application security threats. Finally, we describe our ongoing work in realizing these patterns on top of Rainbow, an existing architecture-based adaptation framework.

We introduce a framework for controlling the charging and discharging processes of plug-in electric vehicles (PEVs) via pricing strategies. Our framework consists of a hierarchical decision-making setting with two layers, which we refer to as aggregator layer and retail market layer. In the aggregator layer, there is a set of aggregators that are requested (and will be compensated for) to provide certain amount of energy over a period of time. In the retail market layer, the aggregator offers some price for the energy that PEVs may provide; the objective is to choose a pricing strategy to incentivize the PEVs so as they collectively provide the amount of energy that the aggregator has been asked for. The focus of this paper is on the decision-making process that takes places in the retail market layer, where we assume that each individual PEV is a price-anticipating decision-maker. We cast this decision-making process as a game, and provide conditions on the pricing strategy of the aggregator under which this game has a unique Nash equilibrium. We propose a distributed consensus-based iterative algorithm through which the PEVs can seek for this Nash equilibrium. Numerical simulations are included to illustrate our results.

Domain-specific languages improve ease-of-use, expressiveness and verifiability, but defining and using different DSLs within a single application remains difficult. We introduce an approach for embedded DSLs where 1) whitespace delimits DSL-governed blocks, and 2) the parsing and type checking phases occur in tandem so that the expected type of the block determines which domain-specific parser governs that block. We argue that this approach occupies a sweet spot, providing high expressiveness and ease-of-use while maintaining safe composability. We introduce the design, provide examples and describe an ongoing implementation of this strategy in the Wyvern programming language. We also discuss how a more conventional keyword-directed strategy for parsing of DSLs can arise as a special case of this type-directed strategy. 

The simplest and purest practical object-oriented language designs today are seen in dynamically-typed languages, such as Smalltalk and Self. Static types, however, have potential benefits for productivity, security, and reasoning about programs. In this paper, we describe the design of Wyvern, a statically typed, pure object-oriented language that attempts to retain much of the simplicity and expressiveness of these iconic designs.

Our goals lead us to combine pure object-oriented and functional abstractions in a simple, typed setting. We present a foundational object-based language that we believe to be as close as one can get to simple typed lambda calculus while keeping object-orientation. We show how this foundational language can be translated to the typed lambda calculus via standard encodings. We then define a simple extension to this language that introduces classes and show that classes are no more than sugar for the foundational object-based language. Our future intention is to demonstrate that modules and other object-oriented features can be added to our language as not more than such syntactical extensions while keeping the object-oriented core as pure as possible.

The design of Wyvern closely follows both historical and modern ideas about the essence of object-orientation, suggesting a new way to think about a minimal, practical, typed core language for objects.

This paper is concerned with the tradeoffs between low-cost heterogenous designs and optimality. We study a class of constrained myopic strategic games on networks which approximate the solutions to a constrained quadratic optimization problem; the Nash equilibria of these games can be found using best-response dynamical systems, which only use local information. The notion of price of heterogeneity captures the quality of our approximations. This notion relies on the structure and the strength of the interconnections between agents. We study the stability properties of these dynamical systems and demonstrate their complex characteristics, including abundance of equilibria on graphs with high sparsity and heterogeneity. We also introduce the novel notions of social equivalence and social dominance, and show some of their interesting implications, including their correspondence to consensus. Finally, using a classical result of Hirsch [1], we fully characterize the stability of these dynamical systems for the case of star graphs with asymmetric interactions. Various examples illustrate our results.

We investigate a notion of behavioral genericity in the context of session type disciplines. To this end, we develop a logically motivated theory of parametric polymorphism, reminiscent of the Girard-Reynolds polymorphic λ-calculus, but casted in the setting of concurrent processes. In our theory, polymorphism accounts for the exchange of abstract communication protocols and dynamic instantiation of heterogeneous interfaces, as opposed to the exchange of data types and dynamic instantiation of individual message types. Our polymorphic session-typed process language satisfies strong forms of type preservation and global progress, is strongly normalizing, and enjoys a relational parametricity principle. Combined, our results confer strong correctness guarantees for communicating systems. In particular, parametricity is key to derive non-trivial results about internal protocol independence, a concurrent analogous of representation independence, and non-interference properties of modular, distributed systems.

This paper proposes a steganography method using the digital images. Here, we are embedding the data which is to be secured into the digital image. Human Visual System proved that the changes in the image edges are insensitive to human eyes. Therefore we are using edge detection method in steganography to increase data hiding capacity by embedding more data in these edge pixels. So, if we can increase number of edge pixels, we can increase the amount of data that can be hidden in the image. To increase the number of edge pixels, multiple edge detection is employed. Edge detection is carried out using more sophisticated operator like canny operator. To compensate for the resulting decrease in the PSNR because of increase in the amount of data hidden, Minimum Error Replacement [MER] method is used. Therefore, the main goal of image steganography i.e. security with highest embedding capacity and good visual qualities are achieved. To extract the data we need the original image and the embedding ratio. Extraction is done by taking multiple edges detecting the original image and the data is extracted corresponding to the embedding ratio.

Many important security informatics problems require consideration of dynamical phenomena for their solution; examples include predicting the behavior of individuals in social networks and distinguishing malicious and innocent computer network activities based on activity traces. While information theory offers powerful tools for analyzing dynamical processes, to date the application of information-theoretic methods in security domains has focused on static analyses (e.g., cryptography, natural language processing). This paper leverages information-theoretic concepts and measures to quantify the similarity of pairs of stochastic dynamical systems, and shows that this capability can be used to solve important problems which arise in security applications. We begin by presenting a concise review of the information theory required for our development, and then address two challenging tasks: 1.) characterizing the way influence propagates through social networks, and 2.) distinguishing malware from legitimate software based on the instruction sequences of the disassembled programs. In each application, case studies involving real-world datasets demonstrate that the proposed techniques outperform standard methods.