Publications
134 results found
Mackay J, Eisenbach S, Noble J, et al., 2022, Necessity specifications for robustness, Proceedings of the ACM on Programming Languages, Vol: 6
Robust modules guarantee to do only what they are supposed to do - even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.
Drossopoulou S, Eisenbach S, 2022, Java is type safe -- probably, Departmental Technical Report: 96/8, Publisher: Department of Computing, Imperial College London
Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather than waiting to find out empirically what damage Java programs do, we aim to examine first the language and then the environment, looking for points of weakness. A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer security.We consider a type safe subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null and arrays. We argue that for this subset the type system is sound, by proving that program execution preserves the types, up to subclasses/subinterfaces.
Tasos A, Franco J, Drossopoulou S, et al., 2020, Reshape your layouts, not your programs: A safe language extension for better cache locality, Science of Computer Programming, Vol: 197, ISSN: 0167-6423
The vast divide between the speed of CPU and RAM means that effective use of CPU caches is often a prerequisite for high performance on modern architectures. Hence, developers need to consider how to place data in memory so as to exploit spatial locality and achieve high memory bandwidth. Such manual memory optimisations are common in unmanaged languages (e.g. C, C++), but they sacrifice readability, maintainability, memory safety, and object abstraction. In managed languages, such as Java and C#, where the runtime abstracts away the memory from the developer, such optimisations are almost impossible.We present a language extension called SHAPES, which aims to offer developers more fine-grained control over the placement of data, without sacrificing memory safety or object abstraction. In SHAPES, programmers group related objects into pools, and specify how objects are laid out in these pools. Classes and types are annotated by pool parameters, which allow placement aspects to be changed orthogonally to the code that operates on the objects in the pool. These design decisions disentangle business logic and memory concerns.We give a formal model of SHAPES, present its type and memory safety model, and present its translation to a low-level language. We argue why we expect this translation to be efficient in terms of runtime representation of objects and access to their fields. We argue that SHAPES can be incorporated into existing managed and unmanaged language runtimes and fit well with garbage collection.
Drossopoulou S, Noble J, MacKay J, et al., 2020, Holistic specifications for robust programs, International Conference on Fundamental Approaches to Software Engineering, Publisher: Springer Verlag, ISSN: 0302-9743
Functional specifications describe what program components can do: the sufficient conditions to invoke components' operations. They allow us to reason about the use of components in a closed world setting, wherecomponents interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component.Sufficient conditions are not enough to reason about the use of components in an \emph{open world} setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time. In this open world setting, we must also consider the possible external code. \emph{necessary} conditions, i.e, what are the conditions without which an effect will not happen. In this paper we propose the Chainmail specification language for writing {holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \Chainmail, and discuss several examples. The core of \Chainmail has been mechanised in the Coq proof assistant.
Drossopoulou S, Noble J, Mackay J, et al., 2020, Holisitic specifications for robust programs - Coq model
A Coq formalism of the core of the Chainmail specification language, along with an underlying language, Loo.This Coq formalism has been developed as part of the associated paper: Holistic Specifications for Robust Programs (https://arxiv.org/abs/2002.08334), to be published at FASE 2020
Kiss C, Field A, Eisenbach S, et al., 2019, Higher-order type-level programming in Haskell, International Conference on Functional Programming, Publisher: ACM, Pages: 1-17, ISSN: 2475-1421
Type family applications in Haskell must be fully saturated. This means that all type-level functions haveto be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension toGHC that removes this restriction. We augment Haskell’s existing type arrow,→, with anunmatchablearrow,↠, that supports partial application of type families without compromising soundness. A soundness proof isprovided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) inthe type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.
Kiss C, Field T, Eisenbach S, et al., 2019, Fork of GHC implementing -XUnsaturatedTypeFamilies for the paper 'Higher-Order Type-Level Programming in Haskell', Publisher: Association for Computing Machinery (ACM)
Schrans F, Hails D, Harkness A, et al., 2019, Flint for safer smart contracts, Publisher: arXiv
The Ethereum blockchain platform supports the execution of decentralisedapplications or smart contracts. These typically hold and transfer digitalcurrency to other parties on the platform; however, they have been subject tonumerous attacks due to the unintentional introduction of bugs. Over a billiondollars worth of currency has been stolen since its release in July 2015. Assmart contracts cannot be updated after deployment, it is imperative that theprogramming language supports the development of robust contracts. We propose Flint, a new statically-typed programming language specificallydesigned for writing robust smart contracts. Flint's features enforce thewriting of safe and predictable code. To encourage good practices, we introduceprotection blocks. Protection blocks restrict who can run code and when (usingtypestate) it can be executed. To prevent vulnerabilities relating to theunintentional loss of currency, Flint Asset traits provide safe atomicoperations, ensuring the state of contracts is always consistent. Writes tostate are restricted, simplifying reasoning about smart contracts.
Tasos A, Franco J, Wrigstad T, et al., 2018, Extending SHAPES for SIMD architectures, Proceedings of the 13th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems, Publisher: ACM Press, Pages: 1-7
SIMD (Single Instruction, Multiple Data) instruction sets are ubiquitous on modern hardware, but rarely used in software projects. A major reason for this is that efficient SIMD code requires data to be laid out in memory in an unconventional manner, forcing developers to explicitly refactor their code and data structures in order to make use of SIMD.In previous work, we proposed SHAPES, an abstract layout specification for enabling memory optimisations for managed, object-oriented languages. In this paper, we explain how, by extending SHAPES with well-known constructs from the literature, which are not specific to SIMD, we can extend SHAPES to compile programs to use SIMD instructions.The resulting language (sketch) seems able to exploit SIMD capabilities without sacrificing ease of development.
Schrans F, Eisenbach S, Drossopoulou S, 2018, Writing safe smart contracts in flint, Pages: 218-219
Blockchain-based platforms such as Ethereum support the execution of versatile decentralized applications, known as smart contracts. These typically hold and transfer digital currency (e.g., Ether) to other parties on the platform. Contracts have been subject to numerous attacks, losing hundreds of millions of dollars (in Ether). We propose Flint, a new type-safe, capabilities-secure, contractoriented programming language specifically designed for writing robust smart contracts. To help programmers reason about access control of functions, Flint programmers use caller capabilities. To prevent vulnerabilities relating to the unintentional loss of currency, transfers of assets in Flint are performed through safe atomic operations, inspired by linear type theory.
Franco J, Hagelin M, Wrigstad T, et al., 2017, You can have it all: Abstraction and good cache performance, 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2017, Publisher: ACM, Pages: 148-167
On current architectures, the optimisation of an application's performance often involves data being stored according to access affinity - what is accessed together should be stored together, rather than logical affinity - what belongs together logically stays together. Such low level techniques lead to faster, but more error prone code, and end up tangling the program's logic with low-level data layout details. Our vision, which we call SHAPES - Safe, High-level, Abstractions for oPtimisation of mEmory cacheS - is that the layout of a data structure should be defined only once, upon instantiation, and the remainder of the code should be layout agnostic. This enables performance improvements while also guaranteeing memory safety, and supports the separation of program logic from low level concerns. In this paper we investigate how this vision can be supported by extending a programming language. We describe the core language features supporting this vision: classes can be customized to support different layouts, and layout information is carried around in types; the remaining source code is layout-unaware and the compiler emits layout-aware code. We then discuss our SHAPES implementation through a prototype library, which we also used for preliminary evaluations. Finally, we discuss how the core could be expanded so as to deliver SHAPES's full potential: the incorporation of compacting garbage collection, ad hoc polymorphism and late binding, synchronization of representations of different collections, support for dynamic change of representation, etc.
Wood T, Drossopoulou S, Lahiri SK, et al., 2017, Modular verification of procedure equivalence in the presence of memory allocation, European Symposium on Programming, Publisher: Springer Verlag, ISSN: 0302-9743
For most high level languages, two procedures are equivalentif they transform a pair of isomorphic stores to isomorphic stores. How-ever, tools for modular checking of such equivalence impose a strongercheck where isomorphism is strengthened to equality of stores. This re-sults in the inability to prove many interesting program pairs with re-cursion and dynamic memory allocation.In this work, we present RIE, a methodology to modularly establishequivalence of procedures in the presence of memory allocation, cyclicdata structures and recursion. Our technique addresses the need for find-ing witnesses to isomorphism with angelic allocation, supports reasoningabout equivalent procedures calls when the stores are only locally iso-morphic, and reasoning about changes in the order of procedure calls.We have implemented RIE by encoding it in the Boogie program verifier.We describe the encoding and prove its soundness.
Sonnex W, Drossopoulou S, Eisenbach S, 2012, Zeno: An automated prover for properties of recursive data structures, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Publisher: Springer Berlin Heidelberg, Pages: 407-421, ISSN: 0302-9743
Most functional programs rely heavily on recursively defined structures and pattern matching thereupon. Proving properties of such programs often requires a proof by induction, which many theorem provers have difficulty addressing. In this paper we present Zeno, a new tool for the automatic verification of simple properties of functional programs. We define a minimal functional language along with a subset of first order logic in which to express properties to be proven. Zeno constructs a proof tree by iteratively reducing the goal into an equivalent conjunction of several simpler sub-goals, terminating when all leaves are trivially true. Building this tree requires the exploration of many alternatives and we give sophisticated techniques for the reduction of this search space through the analysis of function definitions. We provide a comparison with the rippling based tool IsaPlanner and the industrial strength tool ACL2s. Using a test suite from the IsaPlanner website we found that Zeno could prove strictly more properties than either, and in as good times.
Martins P, McCann J, Eisenbach S, 2012, The Environment as an Argument, Practical Aspects of Declarative Languages, Publisher: Springer Berlin Heidelberg, Pages: 48-62
Gudka K, Harris T, Eisenbach S, 2012, Lock inference in the presence of large libraries, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7313 LNCS, Pages: 308-332, ISSN: 0302-9743
Atomic sections can be implemented using lock inference. For lock inference to be practically useful, it is crucial that large libraries be analysed. However, libraries are challenging for static analysis, due to their cyclomatic complexity. Existing approaches either ignore libraries, require library implementers to annotate which locks to take or only consider accesses performed upto one level deep in library call chains. Thus, some library accesses may go unprotected, leading to atomicity violations that atomic sections are supposed to eliminate. We present a lock inference approach for Java that analyses library methods in full. We achieve this by (i) formulating lock inference as an Interprocedural Distributive Environment dataflow problem, (ii) using a graph representation for summary information and (iii) applying a number of optimisations to our implementation to reduce space-time requirements and locks inferred. We demonstrate the scalability of our approach by analysing the entire GNU Classpath library comprising 122KLOC. © 2012 Springer-Verlag Berlin Heidelberg.
Gudka K, Harris T, Eisenbach S, 2012, Lock Inference in the Presence of Large Libraries, European Conference on Object-Oriented Programming, Publisher: Springer, Pages: 308-332, ISSN: 0302-9743
Atomic sections can be implemented using lock inference. For the implementation of lock inference to be practically useful, it is crucial that large libraries be analysed. Large libraries are challenging for static analysis, due to their cyclomatic complexity.Existing approaches either ignore libraries, require library implementers to annotate which locks to take or only consider accesses performed upto one level deep in library call chains. As a result, some accesses performed within the library may go unprotected, leading to atomicity violations that atomic sections are supposed to eliminate.We present a lock inference approach for Java that analyses library methods in full. We achieve this by (i) formulating lock inference as an Interprocedural Distributive Environment dataflow problem, (ii) using a graph representation for summary information and (iii) applying a number of optimisations to our implementation to reduce space-time requirements. We evaluate the effects of each optimisation and show that propagating only new dataflow information gives the biggest speed up whilst also reducing memory usage. We identify and remove many locks for thread-local and internal objects via simple analyses. We demonstrate the scalability of our approach by analysing the entire GNU Classpath library comprising 122KLOC.
Canfora G, Dalcher D, Raffo D, et al., 2011, In memory of Manny Lehman, 'Father of Software Evolution', JOURNAL OF SOFTWARE MAINTENANCE AND EVOLUTION-RESEARCH AND PRACTICE, Vol: 23, Pages: 137-144, ISSN: 1532-060X
- Author Web Link
- Cite
- Citations: 2
Gamrat C, Philippe J-M, Jesshope C, et al., 2011, AETHER: Self-Adaptive Networked Entities: Autonomous Computing Elements for Future Pervasive Applications and Technologies, RECONFIGURABLE COMPUTING: FROM FPGAS TO HARDWARE/SOFTWARE CODESIGN, Editors: Cardoso, Hubner, Publisher: SPRINGER, Pages: 149-184, ISBN: 978-1-4614-0060-8
Allwood T, Cadar C, Eisenbach S, 2011, High Coverage Testing of Haskell Programs, International Symposium on Software Testing and Analysis, Publisher: ACM, Pages: 375-385
This paper presents Irulan, a fully automatic tool designed to perform systematic gray-box unit testing of Haskell libraries. Through automatic code generation and execution, Irulan checks if there are any possible uses of a library's API that cause uncaught exceptions to be thrown. If such cases are found, Irulan returns a Haskell expression that triggers the error, to help programmers debug and fix their code. Irulan supports (and takes advantage of) the most important features of the Haskell language, such as lazy evaluation and polymorphism. In addition, it uses various exploration strategies and caching to more effectively explore the state space of the programs under testing. We evaluate Irulan on over 50 benchmarks from the nofib suite and show that it can effectively generate high-coverage test suites and find errors in these programs.
Allwood TOR, Eisenbach S, 2010, Strengthening the zipper, Electronic Notes in Theoretical Computer Science, Vol: 253, Pages: 3-18, ISSN: 1571-0661
The zipper is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet only scratches the surface of some of its potential applications. In this paper we take inspiration from Huet, and describe a library suitable as an underpinning for structured editors. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused. © 2010 Elsevier B.V. All rights reserved.
Plociniczak H, Eisenbach S, 2010, JErlang: Erlang with Joins, COORDINATION 2010, Publisher: Springer, Pages: 61-75
Erlang is an industrially successful functional language that uses the Actor model for concurrency. It supports the message-passing paradigm by providing pattern-matching over received messages. Unfortunately coding synchronisation between multiple processes is not straightforward. To overcome this limitation we designed and implemented JErlang, a Join-Calculus inspired extension to Erlang. We provide a rich set of language features with our joins. We present implementation details of our two alternative solutions, a library and an altered VM. Our optimisations provide JErlang with good performance.
Allwood T, Peyton Jones S, Eisenbach S, 2009, Finding the needle: Stack Traces for GHC, Haskell'09, Pages: 129-140
Even Haskell programs can occasionally go wrong. Programs calling head on an empty list, and incomplete patterns in function definitions can cause program crashes, reporting little more than the precise location where error was ultimately called. Being told that one application of the head function in your program went wrong, without knowing which use of head went wrong can be infuriating.\r\n\r\nWe present our work on adding the ability to get stack traces out of GHC, for example that our crashing head was used during the evaluation of foo, which was called during the evaluation of bar, during the evaluation of main. We provide a transformation that converts GHC Core programs into ones that pass a stack around, and a stack library that ensures bounded heap usage despite the highly recursive nature of Haskell. We call our extension to GHC StackTrace.
Schaeffer Filho A, Lupu E, Sloman M, et al., 2009, Verification of Policy-based Self-Managed Cell Interactions Using Alloy, IEEE International Symposium on Policies for Distributed Systems and Networks (Policy), Publisher: IEEE, Pages: 37-40
Self-Managed Cells (SMCs) define an infrastructure for building ubiquitous computing applications. An SMC consists of an autonomous administrative domain based on a policy-driven feedback control-loop. SMCs are able to interact with each other and compose with other SMCs to form larger autonomous components. In this paper we present a formal specification of an SMC's behaviour for the analysis and verification of its operation in collaborations of SMCs. These collaborations typically involve SMCs originated from different administrative authorities, and the definition of a formal model has helped us to verify the correctness of their operation when SMCs are composed or federated.
Alpay E, Cutler PS, Eisenbach S, et al., 2009, Changing the Marks Based Culture of Learning through Peer Assisted Tutorials, Washington, DC, 2009 ASEE Annual Conference, Publisher: Taylor and Francis Group, Pages: 17-32
We describe and evaluate an approach to student learning that aims to instil a culture of formative assessment based on peer-assisted learning. The idea is for suitably qualified undergraduates to assist in the running of weekly first-year tutorials. They mark submitted work, provide written and verbal feedback and lead problem solving discussions during tutorials. However, contrary to normal practice, the marks they award do not contribute to the students' year total; all tutorial work becomes essentially voluntary. We report results from a pilot implementation of the scheme over a 12-month period in an engineering department at a leading academic institution. The scheme was such that a comparative and triangulated assessment was possible amongst the students and tutor team. Results show no discernible degradation in student attendance, submission rates and performance in either the weekly exercises or end of year examinations. Important benefits to the peer tutors are also found.
Petrounias A, Eisenbach S, 2009, Fairness for Chorded Languages, Coordination'09, Publisher: Springer
Joins or chords is a concurrency construct that seems to fit well with the object oriented paradigm. Chorded languages are presented with implicit assumptions regarding the fair treatment of processes by the scheduler. We define weak and strong fairness for the Small Chorded Object-Oriented Language (l SCHOOL) which allows the classification of executions as fair. We investigate the liveness behaviour of programs and establish worst-case behaviours in terms of scheduling delays. \r\n\r\nWe discover that weak fairness, although giving the scheduler implementer greater freedom in selecting the next process which is to be executed, is harder to implement than strong fairness; strong fairness benefits from a straightforward implementation, however, imposes many more constraints and limits the selection function of a scheduler. \r\n\r\n
Ayres J, Eisenbach S, 2009, Stage: Python with Actors, International Workshop on Multicore Software Engineering (IWMSE)
Programmers hoping to exploit multi-core processors must split their applications into threads suitable for independent, concurrent execution. The lock-based concurrency of many existing languages is clumsy and error prone -- a barrier to writing fast and correct concurrent code.\r\n\r\nThe Actor model exudes concurrency -- each entity in the model (an Actor) executes concurrently. Interaction is restricted to message passing which prevents many of the errors associated with shared mutable state and locking, the common alternative. By favouring message passing over method calling the Actor model makes distribution straightforward. \r\n\r\nEarly Actor-based languages enjoyed only moderate success, probably because they were before their time. More recent Actor languages have enjoyed greater success, the most successful being Erlang, but the language is functional; a paradigm unfamiliar to many programmers. There is a need for a language that presents a familiar and fast encoding of the Actor model. In this paper we present Stage, our mobile Actor language based on Python.
Schaeffer Filho A, Lupu E, Sloman M, et al., 2009, Verification of Policy-based Self-Managed Cell Interactions Using Alloy
Self-Managed Cells (SMCs) define an infrastructure for building ubiquitous computing applications. An SMC consists of an autonomous administrative domain based on a policy-driven feedback control-loop. SMCs are able to interact with each other and compose with other SMCs to form larger autonomous components. In this paper we present a formal specification of an SMC's behaviour for the analysis and verification of its operation in collaborations of SMCs. These collaborations typically involve SMCs originated from different administrative authorities, and the definition of a formal model has helped us to verify the correctness of their operation when SMCs are composed or federated. The formal specification also enables a better characterisation of the integrity constraints that must be preserved during SMC operation.
Sackman M, Eisenbach S, 2009, Safely Speaking in Tongues: Statically Checking Domain Specific Languages in Haskell, Workshop on Language Descriptions Tools and Applications (LDTA) 2009, Pages: 34-51
Haskell makes it very easy to build and use Domain Specific Languages (DSLs). However, it is frequently the case that a DSL has invariants that can not be easily enforced statically, resulting in runtime checks. This is a great pity given HaskellÆs rich and powerful type system and leads to all the usual problems of dynamic checking. \r\n\r\nWe believe that Domain Specific Languages are becoming more popular: the internet itself is a good example of many DSLs (HTML, CSS, JavaScript, Flash, etc), and more seem to be being added every day; most graphics cards already accept programs written in the DSL OpenGL Shading Language (GLSL); and the predicted growth of heterogeneous CPUs (for example IBMÆs Cell CPU) will demand many different DSLs for the various programming models and instruction sets that become available. \r\n\r\nWe present a technique that allows invariants of any given DSL to be lifted into the Haskell type system. This removes the need for runtime checks of the DSL and prevents programs that violate the invariants of the DSL from ever being compiled or executed. As a result we avoid the pitfalls of dynamic checking and return the user of the DSL to the safety and tranquillity of the strongly statically typed Haskell world. \r\n\r\n
Giachino E, Sackman M, Drossopoulou S, et al., 2009, Softly safely spoken: Role playing for Session Types, Places'09
Session types have made much progress at permitting programs be statically verified concordant with a specified protocol. However, it is difficult to build abstractions of, or encapsulate Session types, thus limiting their flexibility. Global session types add further constraints to communication, by permitting the order of exchanges amongst many participants to be specified. The cost is that the number of participants is statically fixed. \r\n\r\nWe introduce Roles in which, similarly to global session types, the number of roles and the conversations involving roles are statically known, but participants can dynamically join and leave roles and the number of participants within a role is not statically known. Statically defined roles which conform to a specified conversation can be dynamically instantiated, participants can be members of multiple roles simultaneously and can participate in multiple conversations concurrently. \r\n\r\n
Allwood TOR, Eisenbach S, 2009, CLASE: Cursor Library for A Structured Editor, ACM SIGPLAN NOTICES, Vol: 44, Pages: 123-124, ISSN: 0362-1340
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.