Papers Submitted for the Best Paper Award

Papers Submitted:

ID Title Bibliographic Details Impact Statement View Paper Change Paper Details
1 An example of title The bibligraphic info of the paper [Security] the statement goes here... (State in layman's terms why you believe the paper is significant in fewer than 100 words. Here I write [Security] as an example, but there are four categories for this competition [security], [resilience], [formal methods] and [bio]. Write the correct category that you submit your paper to.) View Paper Change Paper Details
2 Programming chemistry in DNA addressable bioreactors H. Fellermann & L. Cardelli, Royal Society Interface 11(99), 2014 We present a formal calculus, termed chemtainer calculus, able to capture the complexity of compartmentalized reaction systems such as populations of possibly nested vesicular compartments. Compartments contain molecular cargo as well as surface markers in the form of DNA single strands. These markers serve as compartment addresses and allow for their targeted transport and fusion, thereby enabling reactions of previously separated chemicals. The overall system organization allows for the setup of programmable chemistry in microfluidic or other automated environments. [formal methods] View Paper Change Paper Details
3 Diagnosability under Weak Fairness V. Germanos, S. Haar, V. Khomenko and S. Schwoon: Diagnosability under Weak Fairness. Proc. of ACSD'2014, Mokhov, A. and Bernardinello, L. (Eds.). IEEE Computing Society Press (2014) 132-141 In partially observed Petri nets, diagnosis is the task of detecting whether or not the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution an occurrence of a fault can eventually be diagnosed. In this paper we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever. We show that a previous approach to WF-diagnosability in the literature has a major flaw, and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. This paper was nominated for a best paper award at ACSD'14, and has been invited to a journal special issue on best papers of ACSD'14. [formal methods] View Paper Change Paper Details
4 Quasispecies in population of compositional assemblies [Gross, Fouxon, Lancet and Markovitch; Quasispecies in population of compositional assemblies; BMC Evolutionary Biology 14:2623 (2014)] Here we have shown how compositional replicators, which are intrinsically different than sequential replicators in both information content and replication mechanism, can obey the classical Eigen-Schuster quasispecies theory. Quasispecies refer to information carriers that undergo self-replication with relatively many errors, and as such exhibit an ‘error-catastrophe’ – a specific replication accuracy below which the population structure breaks down. The best quasispecies example in nature is RNA-viruses, which typically replicate with low fidelity, and are treated with drugs that further decrease this fidelity. This paper demonstrates, for the first time, how compositional replicators are indeed evolvable entities which exhibit an error-catastrophe. [bio] View Paper Change Paper Details
5 Dynamic mechanisms of focal seizure onset Yujiang Wang, Marc Goodfellow, Peter Neal Taylor, Gerold Baier. PLoS Computational Biology. Published: August 14, 2014. DOI: 10.1371/journal.pcbi.1003787 [bio] We present a novel computational model of epileptic seizures that includes important physiological connectivity and reproduces many clinical observations, which has never been attempted before. Apart from reproducing observations, the model offers a conceptually advanced view on focal seizures. Using this view we were able, for the first time, to provide stratification criteria to divide the patient group according to different treatment strategies they should receive. Hence this work provides the foundation for introducing model based diagnosis and treatment for epilepsy in the clinical environment. View Paper Change Paper Details
6 Harvesting high value foreign currency transactions from EMV contactless credit cards without the PIN Martin Emms, Budi Arief, Leo Freitas, Joseph Hannon, Aad van Moorsel. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS'14), pp. 716-726, November 2014. DOI: This paper presents an attack, which allows fraudulent transactions to be collected from EMV contactless credit cards without the cardholder's knowledge. The attack exploits a previously unreported vulnerability in the EMV protocol, which allows EMV contactless cards to approve unlimited value transactions without the cardholder’s PIN when the transaction is in a foreign currency. We found that Visa credit cards will approve foreign currency contactless transactions up to €999,999.99; this side-steps the £20 contactless transaction limit in the UK. Published at CCS'14 (one of the top three security conferences), this paper was covered in BBC, Wired, and other media. The paper has attracted major financial organisations such as Visa Europe to work together on countermeasures and future collaboration. [security] View Paper Change Paper Details
7 Studying the Interplay of Concurrency, Performance, Energy and Reliability with ArchOn – an Architecture-open Resource-driven Cross-layer Modelling Framework A. Rafiev, A. Iliasov, A. Romanovsky, A. Mokhov, F. Xia, A. Yakovlev. 14th International Conference on Application of Concurrency to System Design. IEEE Computer Society. June 2014 This is the first major outcome produced by the Newcastle team in the PRiME program grant. We introduce and evaluate a novel modelling approach (called ArchOn) that allows scalable analysis of complex multi-layered systems by zooming into details of the selected parts. The approach targets multi-layred mani-core systems consisting of application, OS and hardware. We believe it is very general and applicable to analysing various systems in which we need to choose the scope/focus of reasoning. [resilience] View Paper Change Paper Details
8 Verifying Secure Information Flow in Federated Clouds Wen Zeng, Maciej Koutny, Paul Watson: Verifying Secure Information Flow in Federated Clouds. In 2014 IEEE 6th International Conference on Cloud Computing Technology and Science (CloudCom), December 15-18, 2014. In this paper, a dynamic flow sensitive security model for a federated cloud system is proposed within which the Bell-LaPadula rules and cloud security rule can be captured. As a result, one can track and verify the information flow security in federated clouds. This is the first paper showing how Petri nets could be used to represent such a system, making it possible to verify secure information flow in federated clouds using the existing Petri net techniques. This paper is published at 2014 IEEE 6th International Conference on Cloud Computing Technology and Science (CloudCom), which is the main cloud computing conference, and the acceptance rate for full paper was 18% in 2014. [security] View Paper Change Paper Details
9 A Survey and Evaluation of the Existing Tools that Support Adoption of Cloud Computing and Selection of Trustworthy and Transparent Cloud Providers Almanea, M. I., “A Survey and Evaluation of the Existing Tools that Support Adoption of Cloud Computing and Selection of Trustworthy and Transparent Cloud Providers”, presented at the University of Salerno. 6th International Conference on Intelligent Networking and Collaborative Systems, Salerno, Italy. 2014 With a growing number of cloud service providers, potential customers will require methods for selecting trustworthy and appropriate providers. We discuss existing tools, methods and frameworks that promote the adoption of cloud computing models, and the selection of trustworthy cloud service providers. We propose a set of customer’s assurance requirements as a basis for comparative evaluation, and is applied to several popular tools (CSA STAR, CloudTrust Protocol, C.A.RE and Cloud Provider Transparency Scorecard). We describe a questionnaire-based survey in which respondents evaluate the extent to which these tools have been used, and assess their usefulness. The majority of respondents agreed on the importance of using the tools to assist migration to the cloud and, although most respondents have not used the tools, those who have used them reported them helpful. It has been noticed that there might be a relationship between a tool’s compliance to the proposed requirements and the popularity of using these tools, and these results should encourage cloud providers to address customers’ assurance requirements. [Security] View Paper Change Paper Details
10 Non-antibiotic quorum sensing inhibitors acting against N-acyl homoserine lactone synthase as druggable target Chien-Yi Chang, Thiba Krishnan, Hao Wang, Ye Chen, Wai-Fong Yin, Yee-Meng Chong, Li Ying Tan, Teik Min Chong, Kok-Gan Chan. Published in Scientific Reports on 28 November 2014 Now we are entering “post-antibiotic” era. It is urgent to find the novel approaches against bacterial infections. Bacterial quorum sensing, a cell-cell communication, has been considered as the therapeutic target to attenuate bacterial virulence and thus control infection by degrading QS signals or interrupting the perception of signal molecules on responding proteins. Here we report new finding of a novel signal synthase inhibitor which inhibits bacterial virulent factor up to 42%. Molecular docking analysis suggested that the inhibitor interacts with signal synthase substrate binding sites. Our data path the way for novel drug discovery that may serve as the next generation magic bullet which is non-antibiotic based. [bio] View Paper Change Paper Details
11 ZombieCoin: Powering Next-Generation Botnets with Bitcoin Taha Ali, Patrick McCorry, Peter Lee, Feng Hao, accepted to the Second Workshop on Bitcoin Research 2014 (in Assocation with Financial Crypto), accepted 23-11-2014 Botnets are the preeminent source of online crime and arguably the greatest threat to the Internet infrastructure. In this paper, we present ZombieCoin, a botnet command-and-control (C&C) mechanism that runs on the Bitcoin network. ZombieCoin offers considerable advantages over existing C&C techniques, most notably the fact that Bitcoin is designed to resist the very regulatory processes currently used to combat botnets. We believe this is a desirable avenue botmasters may explore in the near future and our work is intended as a first step towards devising effective countermeasures. This paper will be published at the second Bitcoin Workshop @ Financial Cryptography – arguably the best venue for a Bitcoin paper to receive the most attention. Currently, no solutions exists as no one has realized before that this could be a problem. [security] View Paper Change Paper Details
12 Modelling Patterns for Systems of Systems Architectures Claire Ingram, Richard Payne, Simon Perry, Jon Holt, Finn Hansen, Luis Couto. IEEE Systems Conference (SysCon), March 2014 [Resilience] Systems of systems (SoSs) are systems composed of constituents which are independent systems in their own right. Examples include: emergency response systems; road and public transportation networks; and agriculture. An SoS produces an emergent, global behaviour when the constituent systems co-operate, but engineering reliable emergent behaviour is difficult when it can only be produced by independent co-operating systems. Because many civil infrastructures are SoSs, SoS engineering techniques can have significant societal impact, but until recently this has been a field with few published case studies and little in the way of structured foundational science or evidence-based guidelines. This collection of patterns is a novel piece of work in the systems engineering community, which has not used patterns previously to characterise SoS architectures, although we believe such work is important for future experience-based lessons. This paper has greatly raised Newcastle’s visibility in the systems engineering community with many requests for more information coming from practitioners. The paper was awarded "Best Paper" by the IEEE Systems Council and has also attracted attention from SoS working group of the systems engineering organisation INCOSE, including an invitation for Newcastle’s staff to initiate a new tranche of collaborative work with the group. View Paper Change Paper Details
13 ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems F. Shmarov, P. Zuliani, accepted to HSCC 2015, accepted 19/12/2014 [Formal methods] ProbReach is a tool for verifying reachability in stochastic hybrid systems - computing the probability that the system reaches a given state space region. Hybrid systems reachability is decidable only for simple systems, and currently no verification tool can handle hybrid systems with continuous random parameters. We developed an algorithm which given an arbitrarily small epsilon>0 and an hybrid system with continuous random parameters, returns an interval shorter than epsilon guaranteed to contain the exact value of the reachability probability. We validated ProbReach by comparison with Monte Carlo simulations, which also showed that ProbReach can be faster than Monte Carlo. View Paper Change Paper Details
14 Composable Modular Models for Synthetic Biology Goksel Misirli, Jennifer Hallinan, and Anil Wipat, ACM Journal on Emerging Technologies in Computing Systems, 11(3), 2014. [Bio] Synthetic biology has huge potential for developing novel biological applications. However, applications are still small and often designed manually. As the size and complexity of engineered systems increase, computational modelling and simulation becomes crucial. Here, we present a model-driven design approach, and a repository of modular and composable models of biological parts termed standard virtual parts (SVPs). These models are reusable and can be assembled computationally to create systems models, acting as genetic blueprints that encode a desired biological system. Model-driven design and automation using SVPs provides an efficient approach facilitating predictable computational design of large-scale and complex biological systems. View Paper Change Paper Details
15 A Model for Capturing and Replaying Proof Strategies Leo Freitas, Cliff B. Jones, Andrius Velykis and Iain Whiteside, Verified Software: Theories, Tools and Experiments, Lecture Notes in Computer Science 2014, pp 183-199 [Formal Methods] Modern theorem provers can discharge a significant proportion of Proof Obligations (POs) that arise in the use of Formal Methods (FM). Unfortunately, the residual POs require tedious manual guidance. On the positive side, these "difficult" POs tend to fall into families each of which requires only a few key ideas to unlock. This paper outlines a system that can lessen the burden of FM proofs by identifying and characterising ways of discharging POs of a family by tracking an interactive proof of one member of the family. This opens the possibility of capturing ideas --- represented as proof strategies --- from an expert and/or maximising reuse of ideas after changes to definitions. The proposed system has to store a wealth of meta-information about conjectures, which can be matched against previously learned strategies, or can be used to construct new strategies based on expert guidance. View Paper Change Paper Details
16 Quantitative Workflow Resiliency J. Mace, C. Morisset, and A. van Moorsel. In Computer Security - ESORICS 2014, volume 8712 of Lecture Notes in Computer Science, pages 344-361. Springer International Publishing, 2014. [Security] Business goals are commonly reached with workflows of logically ordered tasks executed by users. Security constraints restrict some users executing tasks to make assigning a valid user to each task an extremely complex process, especially considering users may become unavailable or ‘fail’ at runtime. Current solutions deem a workflow non-resilient regardless of how many failure cases make a workflow unassignable (i.e. cannot complete). We define Quantitative Workflow Resiliency, a measure of workflow completion rate given a probabilistic user availability model. The problem of selecting a user for a task is encoded as a Markov Decision Process to optimise success rate. View Paper Change Paper Details
17 Stochastic Model Checking of Genetic Circuits Curtis Madsen, Zhen Zhang, Nicholas Roehner, Chris Winstead, and Chris J. Myers, ACM Journal on Emerging Technologies in Computing Systems, 11(3), 2014. [Formal Methods] Synthetic genetic circuits have a number of exciting potential applications such as cleaning up toxic waste, hunting and killing tumor cells, and producing drugs and bio-fuels more efficiently. When designing and analyzing genetic circuits, researchers are often interested in the probability of observing certain behaviors. For very rare behaviors, it becomes computationally intractable to obtain good results as the number of required simulation runs grows exponentially. It is, therefore, necessary to apply numerical methods to determine these probabilities directly. This article describes how stochastic model checking, a method for determining the likelihood that certain events occur in a system, can be applied to models of genetic circuits. View Paper Change Paper Details

Submit a paper