Item Accepted version Open AccessControl of Energy Storage with Market Impact: Lagrangian Approach and Horizons(Institute for Operations Research and the Management Sciences) Gibbens, RJ; Cruise, James; Flatley, Lisa; Zachary, Stan; Gibbens, Richard [0000-0003-3717-3258]We study the control of large scale energy storage operating in a market. Re-optimization of deterministic models is a common pragmatic approach when prices are stochastic. We apply Lagrangian theory to develop such a model and to establish decision and forecast horizons when storage trading affects these prices, an important aspect of some energy markets. The determination of these horizons also provides a simple and efficient algorithm for the determination of the optimal control. The forecast horizons vary between one and fifteen days in realistic electricity storage examples. These examples suggest that modelling price impact is important. Item Published version Open AccessLeaving on a jet plane: the trade in fraudulently obtained airline tickets.(Springer Science and Business Media LLC, 2018) Hutchings, Alice; Hutchings, Alice [0000-0003-3037-2684]Every day, hundreds of people fly on airline tickets that have been obtained fraudulently. This crime script analysis provides an overview of the trade in these tickets, drawing on interviews with industry and law enforcement, and an analysis of an online blackmarket. Tickets are purchased by complicit travellers or resellers from the online blackmarket. Victim travellers obtain tickets from fake travel agencies or malicious insiders. Compromised credit cards used to be the main method to purchase tickets illegitimately. However, as fraud detection systems improved, offenders displaced to other methods, including compromised loyalty point accounts, phishing, and compromised business accounts. In addition to complicit and victim travellers, fraudulently obtained tickets are used for transporting mules, and for trafficking and smuggling. This research details current prevention approaches, and identifies additional interventions, aimed at the act, the actor, and the marketplace. Item Accepted version Open AccessDeep dip teardown of tubeless insulin pump(2017-09-18) Skorobogatov, Sergei; Skorobogatov, Sergei [0000-0001-9414-6489]This paper introduces a deep level teardown process of a personal medical device - the OmniPod wireless tubeless insulin pump. This starts with mechanical teardown exposing the engineering solutions used inside the device. Then the electronic part of the device is analysed followed by components identification. Finally, the firmware extraction is performed allowing further analysis of the firmware inside the device as well as real-time debugging. This paper also evaluates the security of the main controller IC of the device. It reveals some weaknesses in the device design process which lead to the possibility of the successful teardown. Should the hardware security of the controller inside the device was well thought through, the teardown process would be far more complicated. This paper demonstrates what the typical teardown process of a personal medical device involves. This knowledge could help in improving the hardware security of sensitive devices. Item Accepted version Open AccessThe bumpy road towards iPhone 5c NAND mirroring(2016-09-14) Skorobogatov, Sergei; Skorobogatov, Sergei [0000-0001-9414-6489]This paper is a short summary of a real world mirroring attack on the Apple iPhone 5c passcode retry counter under iOS 9. This was achieved by desoldering the NAND Flash chip of a sample phone in order to physically access its connection to the SoC and partially reverse engineering its proprietary bus protocol. The process does not require any expensive and sophisticated equipment. All needed parts are low cost and were obtained from local electronics distributors. By using the described and successful hardware mirroring process it was possible to bypass the limit on passcode retry attempts. This is the first public demonstration of the working prototype and the real hardware mirroring process for iPhone 5c. Although the process can be improved, it is still a successful proof-of-concept project. Knowledge of the possibility of mirroring will definitely help in designing systems with better protection. Also some reliability issues related to the NAND memory allocation in iPhone 5c are revealed. Some future research directions are outlined in this paper and several possible countermeasures are suggested. We show that claims that iPhone 5c NAND mirroring was infeasible were ill-advised. Item Published version Open AccessOn the Reduction of Computational Complexity of Deep Convolutional Neural Networks.(MDPI AG, 2018-04-23) Maji, Partha; Mullins, Robert; Maji, Partha [0000-0002-1919-1228]; Mullins, Robert [0000-0002-8393-2748]Deep convolutional neural networks (ConvNets), which are at the heart of many new emerging applications, achieve remarkable performance in audio and visual recognition tasks. Unfortunately, achieving accuracy often implies significant computational costs, limiting deployability. In modern ConvNets it is typical for the convolution layers to consume the vast majority of computational resources during inference. This has made the acceleration of these layers an important research area in academia and industry. In this paper, we examine the effects of co-optimizing the internal structures of the convolutional layers and underlying implementation of fundamental convolution operation. We demonstrate that a combination of these methods can have a big impact on the overall speedup of a ConvNet, achieving a ten-fold increase over baseline. We also introduce a new class of fast one-dimensional (1D) convolutions for ConvNets using the Toom-Cook algorithm. We show that our proposed scheme is mathematically well-grounded, robust, and does not require any time-consuming retraining, while still achieving speedups solely from convolutional layers with no loss in baseline accuracy. Item Accepted version Open AccessDataset and metrics for predicting local visible differences(Association for Computing Machinery (ACM), 2018) Wolski, K; Giunchi, D; Ye, N; Didyk, P; Myszkowski, K; Mantiuk, R; Seidel, HP; Steed, A; Mantiuk, RKA large number of imaging and computer graphics applications require localized information on the visibility of image distortions. Existing image quality metrics are not suitable for this task as they provide a single quality value per image. Existing visibility metrics produce visual difference maps, and are specifically designed for detecting just noticeable distortions but their predictions are often inaccurate. In this work, we argue that the key reason for this problem is the lack of large image collections with a good coverage of possible distortions that occur in different applications. To address the problem, we collect an extensive dataset of reference and distorted image pairs together with user markings indicating whether distortions are visible or not. We propose a statistical model that is designed for the meaningful interpretation of such data, which is affected by visual search and imprecision of manual marking. We use our dataset for training existing metrics and we demonstrate that their performance significantly improves. We show that our dataset with the proposed statistical model can be used to train a new CNN-based metric, which outperforms the existing solutions. We demonstrate the utility of such a metric in visually lossless JPEG compression, super-resolution and watermarking. Item Accepted version Open AccessHigh Dynamic Range Imaging Technology.(IEEE, 2017) Artusi, Alessandro; Richter, Thomas; Ebrahimi, Touradj; Mantiuk, Rafal K; Mantiuk, Rafal [0000-0003-2353-0349]Abstract: In this lecture note, we describe high dynamic range (HDR) imaging systems. Such systems are able to represent luminances of much larger brightness and, typically, a larger range of colors than conventional standard dynamic range (SDR) imaging systems. The larger luminance range greatly improves the overall quality of visual content, making it appear much more realistic and appealing to observers. HDR is one of the key technologies in the future imaging pipeline, which will change the way the digital visual content is represented and manipulated today. Item Accepted version Open AccessLangevin Dynamics with Continuous Tempering for High-dimensional Non-convex Optimization.(2017) Ye, Nanyang; Zhu, Zhanxing; Mantiuk, Rafal K; Mantiuk, Rafal [0000-0003-2353-0349]Minimizing non-convex and high-dimensional objective functions is challenging, especially when training modern deep neural networks. In this paper, a novel approach is proposed which divides the training process into two consecutive phases to obtain better generalization performance: Bayesian sampling and stochastic optimization. The first phase is to explore the energy landscape and to capture the"temperature dynamics''. These strategies can overcome the challenge of early trapping into bad local minima and have achieved remarkable improvements in various types of neural networks as shown in our theoretical analysis and empirical experiments. Item Accepted version Open AccessTowards a quality metric for dense light fields.(IEEE, 2017-11-09) Adhikarla, Vamsi Kiran; Vinkler, Marek; Sumin, Denis; Mantiuk, Rafal K; Myszkowski, Karol; Seidel, Hans-Peter; Didyk, Piotr; Mantiuk, Rafal [0000-0003-2353-0349]Light fields become a popular representation of three-dimensional scenes, and there is interest in their processing, resampling, and compression. As those operations often result in loss of quality, there is a need to quantify it. In this work, we collect a new dataset of dense reference and distorted light fields as well as the corresponding quality scores which are scaled in perceptual units. The scores were acquired in a subjective experiment using an interactive light-field viewing setup. The dataset contains typical artifacts that occur in light-field processing chain due to light-field reconstruction, multi-view compression, and limitations of automultiscopic displays. We test a number of existing objective quality metrics to determine how well they can predict the quality of light fields. We find that the existing image quality metrics provide good measures of light-field quality, but require dense reference light-fields for optimal performance. For more complex tasks of comparing two distorted light fields, their performance drops significantly, which reveals the need for new, light-field-specific metrics. Item Open AccessThe case for limited-preemptive scheduling in GPUs for real-time systemsSpliet, R; Mullins, Robert; Mullins, Robert [0000-0002-8393-2748]Many emerging cyber-physical systems, such as autonomous vehicles, have both extreme computation and hard latency requirements. GPUs are being touted as the ideal platform for such applications due to their highly parallel organisation. Unfortunately, while offering the necessary performance, GPUs are currently designed to maximise throughput and fail to offer the necessary hard real-time (HRT) guarantees. In this work we discuss three additions to GPUs that enable them to better meet real-time constraints. Firstly, we provide a quantitative argument for exposing the non-preemptive GPU scheduler to software. We show that current GPUs perform hardware context switches for non-preemptive scheduling in 20-26.5μs on average, while swapping out 60-270KiB of state. Although high, these overheads do not forbid non-preemptive HRT scheduling of real-time task sets. Secondly, we argue that limited-preemption support can deliver large benefits in schedulability with very minor impact on the context switching overhead. Finally, we demonstrate the need for a more predictable DRAM request arbiter to reduce interference caused by processes running on the GPU in parallel. Item Published version Open AccessTactical diagrammatic reasoning(Open Publishing Association, 2017) Linker, S; Burton, J; Jamnik, M; Jamnik, Mateja [0000-0003-2772-2532]Although automated reasoning with diagrams has been possible for some years, tools for diagrammatic reasoning are generally much less sophisticated than their sentential cousins. The tasks of exploring levels of automation and abstraction in the construction of proofs and of providing explanations of solutions expressed in the proofs remain to be addressed. In this paper we take an interactive proof assistant for Euler diagrams, Speedith, and add tactics to its reasoning engine, providing a level of automation in the construction of proofs. By adding tactics to Speedith's repertoire of inferences, we ease the interaction between the user and the system and capture a higher level explanation of the essence of the proof. We analysed the design options for tactics by using metrics which relate to human readability, such as the number of inferences and the amount of clutter present in diagrams. Thus, in contrast to the normal case with sentential tactics, our tactics are designed to not only prove the theorem, but also to support explanation. Item Accepted version Open AccessOpportunities for community awareness platforms in personal genomics and bioinformatics education.(Oxford University Press, 2017-11) Bianchi, Lucia; Liò, Pietro; Lio, Pietro [0000-0002-0540-5053]Precision and personalized medicine will be increasingly based on the integration of various type of information, particularly electronic health records and genome sequences. The availability of cheap genome sequencing services and the information interoperability will increase the role of online bioinformatics analysis. Being on the Internet poses constant threats to security and privacy. While we are connected and we share information, websites and internet services collect various types of personal data with or without the user consent. It is likely that genomics will merge with the internet culture of connectivity. This process will increase incidental findings, exposure and vulnerability. Here we discuss the social vulnerability owing to the genome and Internet combined security and privacy weaknesses. This urges more efforts in education and social awareness on how biomedical data are analysed and transferred through the internet and how inferential methods could integrate information from different sources. We propose that digital social platforms, used for raising collective awareness in different fields, could be developed for collaborative and bottom-up efforts in education. In this context, bioinformaticians could play a meaningful role in mitigating the future risk of digital-genomic divide. Item Accepted version Open AccessENDEAVOUR: A Scalable SDN Architecture For Real-World IXPs.(2017) Antichi, Gianni; Castro, Ignacio; Chiesa, Marco; Fernandes, Eder Leão; Lapeyrade, Remy; Kopp, Daniel; Han, Jong Hun; Bruyere, Marc; Dietzel, Christoph; Gusat, Mitchell; Moore, Andrew W; Owezarski, Philippe; Uhlig, Steve; Canini, Marco; Antichi, Gianni [0000-0002-6063-4975]; Moore, Andrew [0000-0002-5494-9305]Innovation in interdomain routing has remained stagnant for over a decade. Recently, IXPs have emerged as economically-advantageous interconnection points for reducing path latencies and exchanging ever increasing traffic volumes among, possibly, hundreds of networks. Given their far-reaching implications on interdomain routing, IXPs are the ideal place to foster network innovation and extend the benefits of SDN to the interdomain level. In this paper, we present, evaluate, and demonstrate EN- DEAVOUR, an SDN platform for IXPs. ENDEAVOUR can be deployed on a multi-hop IXP fabric, supports a large number of use cases, and is highly-scalable while avoiding broadcast storms. Our evaluation with real data from one of the largest IXPs, demonstrates the benefits and scalability of our solution: ENDEAVOUR requires around 70% fewer rules than alternative SDN solutions thanks to our rule partitioning mechanism. In addition, by providing an open source solution, we invite ev- eryone from the community to experiment (and improve) our implementation as well as adapt it to new use cases. Item Accepted version Open AccessScanning the internet for liveness(Association for Computing Machinery (ACM), 2018) Bano, S; Richter, P; Javed, M; Sundaresan, S; Durumeric, Z; Murdoch, SJ; Mortier, R; Paxson, V; Mortier, Richard [0000-0001-5205-5992]Internet-wide scanning depends on a notion of liveness: does a target IP address respond to a probe packet? However, the interpretation of such responses, or lack of them, is nuanced and depends on multiple factors, including: how we probed, how different protocols in the network stack interact, the presence of filtering policies near the target, and temporal churn in IP responsiveness. Although often neglected, these factors can significantly affect the results of active measurement studies. We develop a taxonomy of liveness which we employ to develop a method to perform concurrent IPv4 scans using ICMP, five TCP-based, and two UDP-based protocols, comprehensively capturing all responses to our probes, including negative and cross-layer responses. Leveraging our methodology, we present a systematic analysis of liveness and how it manifests in active scanning campaigns, yielding practical insights and methodological improvements for the design and the execution of active Internet measurement studies. Item Accepted version Open AccessHDR image reconstruction from a single exposure using deep CNNs(Association for Computing Machinery (ACM), 2017) Eilertsen, G; Kronander, J; Denes, G; Mantiuk, RK; Unger, J; Mantiuk, Rafal [0000-0003-2353-0349]Camera sensors can only capture a limited range of luminance simultaneously, and in order to create high dynamic range (HDR) images a set of different exposures are typically combined. In this paper we address the problem of predicting information that have been lost in saturated image areas, in order to enable HDR reconstruction from a single exposure. We show that this problem is well-suited for deep learning algorithms, and propose a deep convolutional neural network (CNN) that is specifically designed taking into account the challenges in predicting HDR values. To train the CNN we gather a large dataset of HDR images, which we augment by simulating sensor saturation for a range of cameras. To further boost robustness, we pre-train the CNN on a simulated HDR dataset created from a subset of the MIT Places database. We demonstrate that our approach can reconstruct high-resolution visually convincing HDR results in a wide range of situations, and that it generalizes well to reconstruction of images captured with arbitrary and low-end cameras that use unknown camera response functions and post-processing. Furthermore, we compare to existing methods for HDR expansion, and show high quality results also for image based lighting. Finally, we evaluate the results in a subjective experiment performed on an HDR display. This shows that the reconstructed HDR images are visually convincing, with large improvements as compared to existing methods. Item Accepted version Open AccessCrafting interactive decoration(Association for Computing Machinery (ACM), 2017-09-01) Benford, S; Koleva, B; Quinn, A; Thorn, EC; Glover, K; Preston, W; Hazzard, A; Rennick-Egglestone, S; Greenhalgh, C; Mortier, R; Mortier, Richard [0000-0001-5205-5992]© 2017 ACM. everyday artefacts. This involves adorning them with decorative patterns that enhance their beauty while triggering digital interactions when scanned with cameras. These are realized using an existing augmented reality technique that embeds computer readable codes into the topological structures of hand-drawn patterns. We describe a research through design process that engaged artisans to craft a portfolio of interactive artefacts, including ceramic bowls, embroidered gift cards, fabric souvenirs, and an acoustic guitar. We annotate this portfolio with reflections on the crafting process, revealing how artisans addressed pattern, materials, form and function, and digital mappings throughout their craft process. Further reflection on our portfolio reveals how they bridged between human and system perceptions of visual patterns and engaged in a deep embedding of digital interactions into physical materials. Our findings demonstrate the potential for interactive decoration, distilling the craft knowledge involved in creating aesthetic and functional decoration, highlight the need for transparent computer vision technologies, and raise wider issues for HCI's growing engagement with craft. Item Published version Open AccessQuantifying the propagation of distress and mental disorders in social networks.(Springer Science and Business Media LLC, 2018-03-22) Scatà, Marialisa; Di Stefano, Alessandro; La Corte, Aurelio; Liò, Pietro; Di Stefano, Alessandro [0000-0003-4905-3309]; Lio, Pietro [0000-0002-0540-5053]Heterogeneity of human beings leads to think and react differently to social phenomena. Awareness and homophily drive people to weigh interactions in social multiplex networks, influencing a potential contagion effect. To quantify the impact of heterogeneity on spreading dynamics, we propose a model of coevolution of social contagion and awareness, through the introduction of statistical estimators, in a weighted multiplex network. Multiplexity of networked individuals may trigger propagation enough to produce effects among vulnerable subjects experiencing distress, mental disorder, which represent some of the strongest predictors of suicidal behaviours. The exposure to suicide is emotionally harmful, since talking about it may give support or inadvertently promote it. To disclose the complex effect of the overlapping awareness on suicidal ideation spreading among disordered people, we also introduce a data-driven approach by integrating different types of data. Our modelling approach unveils the relationship between distress and mental disorders propagation and suicidal ideation spreading, shedding light on the role of awareness in a social network for suicide prevention. The proposed model is able to quantify the impact of overlapping awareness on suicidal ideation spreading and our findings demonstrate that it plays a dual role on contagion, either reinforcing or delaying the contagion outbreak. Item Accepted version Open AccessScientific Workflows on Clouds with Heterogeneous and Preemptible Instances(IOS Press, 2017) Tordini, F; Aldinucci, M; Viviani, P; Merelli, I; Liò, P; Lio, Pietro [0000-0002-0540-5053] Item Accepted version Open AccessProgramming and proving with classical types(Springer International Publishing, 2017) Matache, C; Gomes, VBF; Mulligan, DP; Borges Ferreira Gomes, Victor [0000-0002-2954-4648]; Mulligan, Dominic [0000-0003-4643-3541]The propositions-as-types correspondence is ordinarily presen- ted as linking the metatheory of typed λ-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigot’s λμ-calculus. In this work, we use the λμ-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value λμ-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in ‘direct style’, and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an inter- preter for a system of proof terms cum programming language—called μML—using Isabelle’s code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover—called μTP— for classical first-order logic, capable of synthesising μML programs from completed tactic-driven proofs. We present example closed μML programs with classical tautologies for types, including some inexpressible as closed programs in the original λμ-calculus, and some example tactic-driven μTP proofs of classical tautologies. Item Published version Open AccessInternational comparison of bank fraud reimbursement: Customer perceptions and contractual terms(Oxford University Press, 2018-06-01) Becker, Ingolf; Hutchings, Alice; Abu-Salma, Ruba; Anderson, Ross John; Bohm, Nicholas; Murdoch, Steven James; Sasse, Angela; Stringhini, Gianluca; Hutchings, Alice [0000-0003-3037-2684]; Anderson, Ross John [0000-0001-8697-5682]We set out to investigate how customers comprehend bank terms and conditions (T&Cs). If T&Cs are incomprehensible, then it is unreasonable to expect customers to comply with them. An expert analysis of 30 bank contracts across 25 countries found that in most cases the contract terms were too vague to be understood; in some cases they differ by product type, and advice can even be contradictory. While many banks allow customers to write PINs down as long as they are disguised and not kept with the card, 20% of banks do not allow PINs to be written down at all, and a handful do not allow PINs to be shared between accounts. We test our findings on 151 participants in Germany, the US and UK. They mostly agree: only 35% fully understand the T&Cs, and 28% find that sections are unclear. There are strong regional variations: Germans find their T&Cs particularly hard to understand, but Americans assume harsher T&Cs than they actually are, and tend to be reassured when they actually read them.