The iframe on this page is empty and contains no contentSkip to content

Department of  Computing

2011 - Technical Reports

Number Report Title
2011/1 Craig Interpolation in Displayable Logics
James Brotherston, Rajeev Gore, 30pp
2011/2 UKAIRO: Internet-Scale Bandwidth Detouring
Thom Haddow, Sing Wang Ho, Cristian Lumezanu, Moez Draief, Peter Pietzuch, 14pp
2011/3 Policies, Norms and Actions: Groundwork for a Framework
Robert Craven, 50pp
2011/4 EBS: Decentralised Slot Synchronisation for Broadcast messaging for Low-power Wireless Embedded Systems
Poonam Yadav, Julie A. McCann, 11pp
2011/5 ASPAL. Proof of soundness and completeness
Domenico Corapi, Alessandra Russo, 7pp
2011/6 Access Control via Belnap Logic: Intuitive, Expressive, and Analyzable Policy Composition
Glenn Bruns, Michael Huth, 35pp
2011/7 Applications of Legendre-Fenchel transformation to computer vision problems
Ankur Handa, Richard A. Newcombe, Adrien Angeli, Andrew J. Davison, 34pp
2011/8 Disease re-classification via integration of biological networks
Kai Sun, Chris Larminie, Natasa Przulj, 72pp
2011/9 Proceedings of ICCSW '11
Andrew V. Jones (editor), 122pp
2011/10 A Simple Abstraction for Complex Concurrent Indexes
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark Wheelhouse, 38pp
2011/11 Towards A Program Logic for JavaScript
Philippa Gardner, Sergio Maffeis, Gareth Smith, 14pp
2011/12 Relationship-Based Access Control:Its Expression and Enforcement Through Hybrid Logic
Glenn Bruns, Michael Huth, Philip Fong, Ida Siahaan, 12pp
2011/13 Safe Software Updates via Multi-version Execution
Petr Hosek, Cristian Cadar, 12pp

Craig Interpolation in Displayable Logics

James Brotherston, Rajeev Gore, 30pp
Report: 2011/1

Download PDF Download

We give a general proof-theoretic method for establishing Craig interpolation for displayable logics, based upon an analysis of the individual proof rules of their display calculi. Using this uniform method, we establish interpolation for a spectrum of display calculi differing in their structural rules, including those for multiplicative linear logic, multiplicative additive linear logic and ordinary classical logic.

Our analysis at the level of proof rules also provides new insights into the reasons why interpolation fails, or seems likely to fail, in many substructural logics. Specifically, we identify contraction as being particularly problematic for interpolation except in special circumstances.


UKAIRO: Internet-Scale Bandwidth Detouring

Thom Haddow, Sing Wang Ho, Cristian Lumezanu, Moez Draief, Peter Pietzuch, 14pp
Report: 2011/2

Download PDF Download

The performance of content distribution on the Internet is crucial for many services. While popular content can be delivered efficiently to users by caching it using content delivery networks, the distribution of less popular content is often constrained by the bandwidth of the Internet path between the content server and the client. Neither can influence the selected path and therefore clients may have to download content along a path that is congested or has limited capacity. We describe UKAIRO, a system that reduces Internet download times by using detour paths with higher TCP throughput. UKAIRO first discovers detour paths among an overlay network of potential detour hosts and then transparently diverts HTTP connections via these hosts to improve the throughput of clients downloading from content servers. Our evaluation shows that by performing infrequent bandwidth measurements between 50 randomly selected PlanetLab hosts, UKAIRO can identify and exploit potential detour paths that increase the median bandwidth to public Internet web servers by up to 80%.


Policies, Norms and Actions: Groundwork for a Framework

Robert Craven, 50pp
Report: 2011/3

Download PDF Download

Constraints on computational agents' behaviour are studied both in work on policy-governed systems|usually as part of work on security or policy-based management in distributed software engineering and also in multi-agent systems research, where the terminology is generally one of `norms' and concepts drawn from deontic logic. Interaction between these treatments, and the research communities that study them, has not been as thorough as it might, for though the perpectives, methods and interests are sometimes diferent, there is a great deal of shared ground. In the current research report, we present a language and tools which can be used for reasoning about and studying the operation of both norms and policies on a multi-agent, or distributed, system. The language is based on one member, C+, of a family of knowledge representation formalisms studied in AI. We describe the types of domains that can be represented, the kinds of analysis tasks that are possible, and describe our current implementation (which is freely available for download). Future directions for this work are described.


EBS: Decentralised Slot Synchronisation for Broadcast messaging for Low-power Wireless Embedded Systems

Poonam Yadav, Julie A. McCann, 11pp
Report: 2011/4

Download PDF Download

In this paper, we present a decentralised scheme that facilitates reliable network wide broadcast messaging without the requirement of strict time synchronisation, for duty-cycled low-power wireless embedded systems. In this emergent broadcast slot (EBS) scheme, devices coordinate their wake-up periods with their neighbours to exchange schedule information locally. This leads to the emergence of local slot synchronisation without the need for either network-wide synchronisation or a centralised time synchronisation element. We theoretically show that this scheme converges faster than similar emergent and gradient-based approaches, which we confirm by evaluation on real test-beds. We also show that our scheme exhibits lower overheads while being more tolerant to disturbances caused by faulty nodes, wireless link failures, contention and interference in presence of deterministic propagation delays.


ASPAL. Proof of soundness and completeness

Domenico Corapi, Alessandra Russo, 7pp
Report: 2011/5

Download PDF Download

We provide here a brief introduction and proof of soundness and completeness of the ILP system ASPAL. This document is in support of our ICLP 2011 submission, for the reviewers' benefits.


Access Control via Belnap Logic: Intuitive, Expressive, and Analyzable Policy Composition

Glenn Bruns, Michael Huth, 35pp
Report: 2011/6

Download PDF Download

Access control to IT systems increasingly relies on the ability to compose policies. Hence there is benefit in any framework for policy composition that is intuitive, formal (and so "analyzable" and "implementable"), expressive, independent of specific application domains, and yet able to be extended to create domain-specific instances. Here we develop such a framework based on Belnap logic. An access-control policy is interpreted as a four-valued predicate that maps access requests to either grant, deny, conflict, or unspecified the four values of the Belnap bilattice. We define an expressive access-control policy language PBel, having composition operators based on the operators of Belnap logic. Natural orderings on policies are obtained by lifting the truth and information orderings of the Belnap bilattice. These orderings lead to a query language in which policy analyses, for example, conflict freedom, can be specified. Policy analysis is supported through a reduction of the validity of policy queries to the validity of propositional formulas on predicates over access requests. We evaluate our approach through firewall policy and RBAC policy examples, and discuss domain-specific and generic extensions of our policy language.


Applications of Legendre-Fenchel transformation to computer vision problems

Ankur Handa, Richard A. Newcombe, Adrien Angeli, Andrew J. Davison, 34pp
Report: 2011/7

Download PDF Download

We aim to provide a small background on Lengenre-Fenchel transformation, the applications of which have been increasingly getting popular in computer vision. A general motivation follows up with standard examples. Then we take a good view on their applications in solving various standard computer vision problems e.g. image denoising, optical flow, image deconvolution etc.


Disease re-classification via integration of biological networks

Kai Sun, Chris Larminie, Natasa Przulj, 72pp
Report: 2011/8

Download PDF Download

Currently, human diseases are classified as they were in the late 19th century, by considering only symptoms of the affected organ. With a growing body of transcriptomic, proteomic, metabolomic and genomics data sets describing diseases, we ask whether the old classification still holds in the light of modern biological data. We propose to redefine human disease classification by considering diseases as systems- level disorders of the entire cellular system. To do this, we will integrate different types of biological data mentioned above. A network-based mathematical model will be designed to represent these integrated data, and computational algorithms and tools will be developed and implemented for its analysis.


Proceedings of ICCSW '11

Andrew V. Jones (editor), 122pp
Report: 2011/9

Download PDF Download

This volume contains the proceedings of the inaugural Imperial College Student Workshop (ICCSW '11). The workshop took place on the 29th and 30th of September 2011 and was hosted at Imperial College London. ICCSW is a student-focused and student-organised workshop, featuring exclusively student authored, or co-authored, papers.


A Simple Abstraction for Complex Concurrent Indexes

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark Wheelhouse, 38pp
Report: 2011/10

Download PDF Download

Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes that are accessed concurrently. We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B-Link trees. The complexity of these algorithms, in particular the B-Link tree algorithm, can be completely hidden from the client's view by our abstract specification.


Towards A Program Logic for JavaScript

Philippa Gardner, Sergio Maffeis, Gareth Smith, 14pp
Report: 2011/11

Download PDF Download

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and "with". We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.


Relationship-Based Access Control:Its Expression and Enforcement Through Hybrid Logic

Glenn Bruns, Michael Huth, Philip Fong, Ida Siahaan, 12pp
Report: 2011/12

Download PDF Download

Access control policy is typically defined in terms of attributes, but in many applications it is more natural to define permissions in terms of relationships that resources, systems, and contexts may enjoy. The paradigm of relationship-based access control has been proposed to address this issue, and modal logic has been used as a technical foundation. We argue here that hybrid logic -- a natural and well-established extension of modal logic -- addresses limitations in the ability of modal logic to express certain relationships. Also, hybrid logic has advantages in the ability to efficiently compute policy decisions relative to a relationship graph. We identify a fragment of hybrid logic to be used for expressing relationship-based access-control policies, show that this fragment supports important policy idioms, and study its expressiveness. We also capture the previously studied notion of relational policies in a static type system. Finally, we point out that use of our hybrid logic removes an exponential penalty in existing attempts of specifying complex relationships such as "at least three friends".


Safe Software Updates via Multi-version Execution

Petr Hosek, Cristian Cadar, 12pp
Report: 2011/13

Download PDF Download

Software systems are constantly evolving, with new versions and patches being released on a continuous basis. Unfortunately, software updates present a high risk, with many releases introducing new bugs and security vulnerabilities. We tackle this problem using a simple but effective multi- version based approach. Whenever a new update becomes available, instead of upgrading the software to the new version, we run the new version in parallel with the old; by carefully coordinating their executions and selecting the behavior of the more reliable version when they diverge, we create a more secure and dependable multi-version application. We have implemented this technique in a prototype system targeting multicore processors, and show that it can be applied successfully to several security-critical applications, such as lighttpd and redis.


 

Main campus address:
Imperial College London, South Kensington Campus, London SW7 2AZ, tel: +44 (0)20 7589 5111
Campus maps and information | About this site