This special issue collects selected articles from the Third International Workshop on Linearity (LINEARITY 2014), which was held in Vienna, on July 13th, 2014. The workshop was a one-day satellite event of FLoC 2014, the sixth Federated Logic Conference, which was held as part of the 2014 Vienna Summer of Logic.

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades.

Recent work has investigated the use of hardware performance counters (HPCs) for the detection of malware running on a system. These works gather traces of HPCs for a variety of applications (both malicious and non-malicious) and then apply machine learning to train a detector to distinguish between benign applications and malware. In this work, we provide a more comprehensive analysis of the applicability of using machine learning and HPCs for a specific subset of malware: kernel rootkits.

We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of barbed preorder for a CCS-like process calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely simulation and labelled transition systems. This result establishes a connection between an approach to reason about process specifications, the barbed preorder, and a method to reason about logic specifications, the logical preorder.

The inclusive permissions structure (e.g., the Intel ring model) of modern commodity CPUs provides privileged system software layers with arbitrary permissions to access and modify client processes, allowing them to manage these clients and the system resources efficiently. Unfortunately, these inclusive permissions allow a compromised high-privileged software layer to perform arbitrary malicious activities. In this article, our goal is to prevent attacks that cross system layers while maintaining the abilities of system software to manage the system and allocate resources. In particular, we present a hardware-supported page permission framework for physical pages that is based on the concept of noninclusive sets of memory permissions for different layers of system software (such as hypervisors, operating systems, and user-level applications). Instead of viewing privilege levels as an ordered hierarchy with each successive level being more privileged, we view them as distinct levels each with its own set of permissions. In order to enable system software to manage client processes, we define a set of legal permission transitions that support resource allocation but preserve security. We show that the model prevents a range of recent attacks. We also show that it can be implemented with negligible performance overhead (both at load time and at runtime), low hardware complexity, and minimal changes to the commodity OS and hypervisor code.

Orchestrating a time sensitive computation across an ad hoc ensemble of Android devices is surprisingly challenging in spite of the OS's support for automated network time synchronization. In fact, the lack of access to programmatic nor end-user control pushes the responsibility of implementing fine-grained time synchronization to the application development level. In this paper, we extend CoMingle, a distributed logic programming framework designed for orchestrating Android ensembles, with explicit time annotations and built-in network time synchronization support. The result is a powerful programmable orchestration framework for developing apps that exhibits time-synchronized events across an ensemble of Android devices.

This paper introduces an abstract web programming language, QWeSST, and a methodology for proving properties of formalisms, such are QWeSST, that are parallel, distributed and concurrent. At its core, QWeSST is a small functional programming language extended with primitives for mobile code and remote procedure calls, two distinguishing features of web programming. It supports a localized view of typechecking and of evaluation, which reflects the way we program web applications and web services. We have developed a prototype implementation for QWeSST and used it to elegantly write simple web applications that are however not easily expressed using current web technology. We give two semantics for QWeSST, one is standard and models a naive form of single-threaded evaluation, the other is maximally parallel and exploits a presentation of its typing and execution behaviors based on an extended form of substructural operational semantics. It augments standard inference rules with a construction that realizes parametric multiset comprehension, which makes it convenient to capture ensemble-level behaviors. We prove that both semantics are type safe, the former using traditional methods, the latter by developing a proof methodology that parallels the multiset-oriented presentation of the semantics.

CHR is a declarative, concurrent and committed choice rule-based constraint programming language. In this paper, we adapt CHR to provide a decentralized execution model for parallel and distributed programs. Specifically, we consider an execution model consisting of an ensemble of computing entities, each with its own constraint store and each capable of communicating with its neighbors. We extend CHR into CHRe, in which rules are executed at a location and are allowed to access the constraint store of its immediate neighbors. We give an operational semantics for CHRe, denoted ω0e, that defines incremental and asynchronous decentralized rewriting for the class of CHRe rules characterized by purely local matching (0-neighbor restricted rules). We show the soundness of the ω0e semantics with respect to the abstract CHR semantics. We then give a safe encoding of the more general 1-neighbor restricted rules as 0-neighbor restricted rules, and discuss how this encoding can be generalized to all CHRe programs.

Practical algorithms have been proposed to efficiently recompute the logical consequences of a Datalog program after a new fact has been asserted or retracted. This is essential in a dynamic setting where facts are frequently added and removed. Yet while assertion is logically well understood as incremental inference, the monotonic nature of first-order logic is ill-suited to model retraction. As such, the traditional logical interpretation of Datalog offers at most an abstract specification of Datalog systems, but has tenuous relations to the algorithms that perform efficient assertions and retractions in practical implementations. This paper proposes a logical interpretation of Datalog based on linear logic. It not only captures the meaning of Datalog updates, but also provides an operational model that underlies the dynamic changes of the set of inferable facts, all within the confines of logic. We prove the correctness of this interpretation with respect to its traditional counterpart.

Abstract In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.

This paper describes a new experimental course introduced in the Spring of 2010 at Carnegie Mellon University in Qatar. Discovering Logic is an introduction to logic for Computer Science majors in their freshman year. It targets students who have had little or no exposure to logic and has the primary objective of 1) preparing them for sophomore classes which require proficiency with understanding formal statements expressed in English, elementary reasoning skills, and a sense of mathematical rigor. The course is structured as to achieve two additional objectives: 2) develop the students' communication skills, and 3) give them some historical depth into Computer Science and logic. This led to a somewhat unconventional approach that used a comic book, Logicomix, as the course textbook and that empowered the students to be active agents in the learning process through presentations and numerous open discussions. Preliminary analysis hints at an improved performance in follow-up courses, indicating that it may be achieving its primary objective.

In the last decade or so, the ACM, the IEEE and other organizations have acknowledged that there is a problem with the way communication is taught in the Computer Science curriculum: the writing, speaking, and presentation skills students learn in the classroom do not match what is expected of them in the workplace. The proposed solution, adopted by many undergraduate colleges, was to add a technical communication course to the CS curriculum. This does not appear to be enough, as mainstream accreditation boards are still emphasizing the need for improvement of communication skills instruction in their recent reports and recommendations. For the last two years, we have experimented with a complementary transversal approach where many "traditional CS" courses in our program have added a communication component to their syllabus, while at the same time our technical communication course has been revamped to expose students to realistic practices as promoted by situated learning theory. The results, so far anecdotal, point to improved student performance and attitude across several communication dimensions, in particular writing and presentation. We plan to develop this experiment by spreading it across more classes and by starting to collect rigorous measurements of students' communication performance.

In this paper, we show how we can increase the ease of reading and writing security requirements for cryptographic protocols at the Dolev-Yao level of abstraction by developing a visual language based on fault trees. We develop such semantics for a subset of NRL protocol analyzer temporal requirements language (NPATRL), a temporal language used for expressing safety requirements for cryptographic protocols, and show that the subset is sound and complete with respect to the semantics. We also show how the fault trees can be used to improve the presentation of some specifications that we developed in our analysis of the group domain of interpretation (GDOI) protocol. Other examples involve a property of Kerberos 5 and a visual account of the requirements in Lowe's authentication hierarchy.

Authentication and secrecy properties are proved by very different methods: the former by local reasoning, leading to matching knowledge of all principals about the order of their actions, the latter by global reasoning towards the impossibility of knowledge of some data. Hence, proofs conceptually decompose in two parts, each encapsulating the other as an assumption. From this observation, we develop a simple logic of authentication that encapsulates secrecy requirements as assumptions. We apply it within the derivational framework to derive a large class of key distribution protocols based on the authentication properties of their components.

When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly de

Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev–Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Strand spaces provide a simple and economical approach to analysis of completed protocol runs by emphasizing causal interactions among protocol participants. The multiset rewriting formalism provides a very precise way of specifying finite-length protocols with unboundedly many instances of each protocol role, such as client, server, initiator, or responder. A number of modifications to each system are required to produce a meaningful comparison. In particular, we extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands. The relationship we illustrate here between multiset rewriting specifications and strand spaces thus suggests refinements to both frameworks, and deepens our understanding of the Dolev–Yao model.

Although research has been going on in the formal analysis of cryptographic protocols for a number of years, they are only slowly being integrated into the protocol design process. In this paper we describe how we furthered the integration of analysi

We present the spine calculus S→⊸&⊤ as an efficient representation for the linear λ-calculus λ→⊸&⊤ which includes unrestricted functions (→) linear functions (⊸) additive pairing (&) and additive unit (⊤). S→⊸&⊤ enhances the representation of Church's simply typed λ-calculus by enforcing extensionality and by incorporating linear constructs. This approach permits procedures such as unification to retain the efficient head access that characterizes first-order term languages without the overhead of performing η-conversions at run time. Applications lie in proof search, logic programming, and logical frameworks based on linear type theories. It is also related to foundational work on term assignment calculi for presentations of the sequent calculus. We define the spine calculus, give translations of λ→⊸&⊤ into S→⊸&⊤ and vice versa, prove their soundness and completeness with respect to typing and reductions, and show that the typable fragment of the spine calculus is strongly normalizing and admits unique canonical, i.e. βη-normal, forms.

We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not been previously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate some of these anomalies.

Formal analysis of security protocols is largely based on an set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiuser rewriting with existential quantification. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the stand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands.

Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language λProlog and prove the soundness and completeness of the resulting logic programs.

Most formal approaches to security protocol analysis are based on a set of assumptions commonly referred to as the "Dolev-Yao model". In this paper, we use a multiset rewriting formalism, based on linear logic, to state the basic assumptions of this model. A characteristic of our formalism is the way that existential quantification provides a succinct way of choosing new values, such as new keys or nonces. We define a class of theories in this formalism that correspond to finite-length protocols, with a bounded initialization phase but allowing unboundedly many instances of each protocol role (e.g., client, sewer; initiator or responder). Undecidability is proved for a restricted class of these protocols, and PSPACE-completeness is claimed for a class further restricted to have no new data (nonces). Since it is a fragment of linear logic, we can use our notation directly as input to linear logic tools, allowing us to do proof search for attacks with relatively little programming effort, and to formally verify protocol transformations and optimizations.

We develop an efficient representation and a pre-unification algorithm in the style of Huet (1975) for the linear /spl lambda/-calculus /spl lambda//sup /spl rarr//spl rArr/0&T/ which includes intuitionistic functions (/spl rarr/), linear functions (/spl rArr/), additive pairing (&), and additive unit (T). Applications lie in proof scorch, logic programming, and logical frameworks based on linear type theories. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages.

We present the linear type theory LLF as the formal basis for a conservative extension of the LF logical framework. LLF combines the expressive power of dependent types with linear logic to permit the natural and concise representation of a whole new class of deductive systems, namely those dealing with state. As an example we encode a version of Mini-ML with references including its type system, its operational semantics, and a proof of type preservation. Another example is the encoding of a sequent calculus for classical linear logic and its cut elimination theorem. LLF can also be given an operational interpretation as a logic programming language under which the representations above can be used for type inference, evaluation and cut-elimination.