HASLab - Other Publications

Permanent URI for this collection

http://localhost:4000/handle/123456789/186

Browse

Browsing HASLab - Other Publications by Issue Date

Jump to a point in the index:
  • Item
    On the semantic security of functional encryption schemes
    ( 2013) Manuel Barbosa ; Farshim,P
    Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O'Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive token-extraction attack scenarios that shed further light on the potential reach of general FE for practical applications. © 2013 International Association for Cryptologic Research.
  • Item
    Interactive interaction constraints
    ( 2013) José Paiva Proença ; Clarke,D
    Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction. This paper introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using two examples, a hotel booking system and a system of transactions with compensations. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine. © 2013 IFIP International Federation for Information Processing.
  • Item
    Interactive Verification of Safety-Critical Software
    ( 2013) da Cruz,D ; Henriques,PR ; Jorge Sousa Pinto
    A central issue in program verification is the generation of verification conditions (VCs): proof obligations which, if successfully discharged, guarantee the correctness of a program vis-a-vis a given specification. While the basic theory of program verification has been around since the 1960s, the late 1990s saw the advent of practical tools for the verification of realistic programs, and research in this area has been very active since then. Automated theorem provers have contributed decisively to these developments. This paper establishes a basis for the generation of verification conditions combining forward and backward reasoning, for programs consisting of mutually-recursive procedures annotated with contracts and loop invariants. We introduce also a visual technique to verify a program, in an interactive way, using Verification Graphs (VG), where a VG is a Control Flow Graph (CFG) whose edges are labeled with contracts (pre- and postconditions). This technique intends to help a software engineer to find statements that are not valid with respect to the program's specification.
  • Item
    Querying model-driven spreadsheets
    ( 2013) Jácome Costa Cunha ; João Paulo Fernandes ; Jorge Cunha Mendes ; Rui Alexandre Pereira ; João Alexandre Saraiva
    Spreadsheets are being used with many different purposes that range from toy applications to complete information systems. In any of these cases, they are often used as data repositories that can grow significantly. As the amount of data grows, it also becomes more difficult to extract concrete information out of them. This paper focuses on the problem of spreadsheet querying. In particular, we propose an expressive and composable technique where intuitive queries can be defined. Our approach builds on a model-driven spreadsheet development environment, and queries are expressed referencing entities in the model of a spreadsheet instead of in its actual data. Finally, the system that we have implemented relies on Google's query function for spreadsheets. © 2013 IEEE.
  • Item
    Automated theorem proving for the systematic analysis of an infusion pump
    ( 2013) Michael Douglas Harrison ; Paolo Masci ; José Creissac Campos ; Curzon,P
  • Item
    A Generic Scheme and Properties of Bidirectional Transformations
    ( 2013) Hugo Pereira Pacheco ; Nuno Moreira Macedo ; Alcino Cunha ; Voigtländer,Janis
  • Item
    Data Abstraction in Coordination Constraints
    ( 2013) José Paiva Proença ; Clarke,D
    This paper studies complex coordination mechanisms based on constraint satisfaction. In particular, it focuses on data-sensitive connectors from the Reo coordination language. These connectors restrict how and where data can flow between loosely-coupled components taking into account the data being exchanged. Existing engines for Reo provide a very limited support for data-sensitive connectors, even though data constraints are captured by the original semantic models for Reo. When executing data-sensitive connectors, coordination constraints are not exhaustively solved at compile time but at runtime on a per-need basis, powered by an existing SMT (satisfiability modulo theories) solver. To deal with a wider range of data types and operations, we abstract data and reduce the original constraint satisfaction problem to a SAT problem, based on a variation of predicate abstraction. We show soundness and completeness of the abstraction mechanism for well-defined constraints, and validate our approach by evaluating the performance of a prototype implementation with different test cases, with and without abstraction. © Springer-Verlag Berlin Heidelberg 2013.
  • Item
    QuerySheet: A bidirectional query environment for model-driven spreadsheets
    ( 2013) Belo,O ; Jácome Costa Cunha ; João Paulo Fernandes ; Jorge Cunha Mendes ; Rui Alexandre Pereira ; João Alexandre Saraiva
    This paper presents a tool, named QuerySheet, to query spreadsheets. We defined a language to write the queries, which resembles SQL, the language to query databases. This allows to write queries which are more related to the spreadsheet content than with current approaches. © 2013 IEEE.
  • Item
    A Model-based Approach for Test Cases Generation
    ( 2013) Silva,JC ; José Luís Silva ; José Creissac Campos ; João Alexandre Saraiva
    The analytical methods based on evaluation models of interactive systems were proposed as an alternative to user testing in the last stages of the software development due to its costs. However, the use of isolated behavioral models of the system limits the results of the analytical methods. An example of these limitations relates to the fact that they are unable to identify implementation issues that will impact on usability. With the introduction of model-based testing we are enable to test if the implemented software meets the specified model. This paper presents an model-based approach for test cases generation from the static analysis of source code.
  • Item
    Executable modelling of dynamic software product lines in the ABS language
    ( 2013) Muschevici,R ; Clarke,D ; José Paiva Proença
    Dynamic software product lines (DSPLs) combine the advantages of traditional SPLs, such as an explicit variability model connected to an integrated repository of reusable code artefacts, with the ability to exploit a system's variability at runtime. When a system needs to adapt, for example to changes in operational environment or functional requirements, DSPL systems are capable of adapting their behaviour dynamically, thus avoiding the need to halt, recompile and redeploy. The field of DSPL engineering is still in formation and general-purpose DSPL development languages and tools are rare. In this paper we introduce a language and execution environment for developing and running dynamic SPLs. Our work builds on ABS, a language and integrated development environment with dedicated support for implementing static software product lines. Our ABS extension advances the scope of ABS to dynamic SPL engineering. Systems developed using ABS are compiled to Java, and are thus executable on a wide range of platforms. Copyright 2013 ACM.
  • Item
    DATAFLASKS: an epidemic dependable key-value substrate
    ( 2013) Francisco Almeida Maia ; Miguel Marques Matos ; Ricardo Pereira Vilaça ; José Orlando Pereira ; Rui Carlos Oliveira ; Riviere,E
    Recently, tuple-stores have become pivotal structures in many information systems. Their ability to handle large datasets makes them important in an era with unprecedented amounts of data being produced and exchanged. However, these tuple-stores typically rely on structured peer-to-peer protocols which assume moderately stable environments. Such assumption does not always hold for very large scale systems sized in the scale of thousands of machines. In this paper we present a novel approach to the design of a tuple-store. Our approach follows a stratified design based on an unstructured substrate. We focus on this substrate and how the use of epidemic protocols allow reaching high dependability and scalability.
  • Item
    Towards a mostly-automated prover for bit-vector arithmetic
    ( 2013) Abal,I ; Jorge Sousa Pinto
    We present work in progress on the development of EasyBV, a specialized theorem prover for fixed-size bit-vector arithmetic. © 2013 Authors.
  • Item
    On the relationship between functional encryption, obfuscation, and fully homomorphic encryption
    ( 2013) Alwen,J ; Manuel Barbosa ; Farshim,P ; Gennaro,R ; Gordon,SD ; Tessaro,S ; Wilson,DA
    We investigate the relationship between Functional Encryption (FE) and Fully Homomorphic Encryption (FHE), demonstrating that, under certain assumptions, a Functional Encryption scheme supporting evaluation on two ciphertexts implies Fully Homomorphic Encryption. We first introduce the notion of Randomized Functional Encryption (RFE), a generalization of Functional Encryption dealing with randomized functionalities of interest in its own right, and show how to construct an RFE from a (standard) semantically secure FE. For this we define the notion of entropically secure FE and use it as an intermediary step in the construction. Finally we show that RFEs constructed in this way can be used to construct FHE schemes thereby establishing a relation between the FHE and FE primitives. We conclude the paper by recasting the construction of RFE schemes in the context of obfuscation. © 2013 Springer-Verlag Berlin Heidelberg.
  • Item
    Combining static and dynamic analysis for the reverse engineering of Web applications
    ( 2013) Silva,CE ; José Creissac Campos
    Software has become so complex that it is increasingly hard to have a complete understanding of how a particular system will behave. Web applications, their user interfaces in particular, are built with a wide variety of technologies making them particularly hard to debug and maintain. Reverse engineering techniques, either through static analysis of the code or dynamic analysis of the running application, can be used to help gain this understanding. Each type of technique has its limitations. With static analysis it is difficult to have good coverage of highly dynamic applications, while dynamic analysis faces problems with guaranteeing that generated models fully capture the behavior of the system. This paper proposes a new hybrid approach for the reverse engineering of web applications' user interfaces. The approach combines dynamic analyzes of the application at runtime, with static analyzes of the source code of the event handlers found during interaction. Information derived from the source code is both directly added to the generated models, and used to guide the dynamic analysis. Copyright 2013 ACM.
  • Item
    Formal verification of side-channel countermeasures using self-composition
    ( 2013) José Bacelar Almeida ; Manuel Barbosa ; Jorge Sousa Pinto ; Vieira,B
    Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-composition proofs of non-interference and generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on self-composition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.
  • Item
    Depth Cues and Perceived Audiovisual Synchrony of Biological Motion
    ( 2013) Carlos Loureiro Silva ; Mendonca,C ; Mouta,S ; Silva,R ; José Creissac Campos ; Santos,J
    Background: Due to their different propagation times, visual and auditory signals from external events arrive at the human sensory receptors with a disparate delay. This delay consistently varies with distance, but, despite such variability, most events are perceived as synchronic. There is, however, contradictory data and claims regarding the existence of compensatory mechanisms for distance in simultaneity judgments. Principal Findings: In this paper we have used familiar audiovisual events - a visual walker and footstep sounds and manipulated the number of depth cues. In a simultaneity judgment task we presented a large range of stimulus onset asynchronies corresponding to distances of up to 35 meters. We found an effect of distance over the simultaneity estimates, with greater distances requiring larger stimulus onset asynchronies, and vision always leading. This effect was stronger when both visual and auditory cues were present but was interestingly not found when depth cues were impoverished. Significance: These findings reveal that there should be an internal mechanism to compensate for audiovisual delays, which critically depends on the depth information available.
  • Item
    Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations
    ( 2013) José Bacelar Almeida ; Manuel Barbosa ; Barthe,G ; Dupressoir,F
    We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealized components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework by applying it to the RSA-OAEP encryption scheme, as standardized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it bridges the gap between computer-assisted security proofs and real-world cryptographic implementations as described by standards such as PKCS,and demonstrates the use of the CompCert certified compiler in the context of cryptographic software development. © 2013 ACM.
  • Item
    Slicing as a Distributed Systems Primitive
    ( 2013) Francisco Almeida Maia ; Miguel Marques Matos ; Rui Carlos Oliveira ; Riviere,E
    Large-scale distributed systems appear as the major infrastructures for supporting planet-scale services. These systems call for appropriate management mechanisms and protocols. Slicing is an example of an autonomous, fully decentralized protocol suitable for large-scale environments. It aims at organizing the system into groups of nodes, called slices, according to an application-specific criteria where the size of each slice is relative to the size of the full system. This allows assigning a certain fraction of nodes to different task, according to their capabilities. Although useful, current slicing techniques lack some features of considerable practical importance. This paper proposes a slicing protocol, that builds on existing solutions, and addresses some of their frailties. We present novel solutions to deal with non-uniform slices and to perform online and dynamic slices schema reconfiguration. Moreover, we describe how to provision a slice-local Peer Sampling Service for upper protocol layers and how to enhance slicing protocols with the capability of slicing over more than one attribute. Slicing is presented as a complete, dependable and integrated distributed systems primitive for large-scale systems.
  • Item
    Scalable Eventually Consistent Counters over Unreliable Networks
    ( 2013) Paulo Sérgio Almeida ; Carlos Baquero
  • Item
    Spatial limits for audiovisual unity assumption
    ( 2014) Carlos Loureiro Silva ; Sandra Silva Mouta ; José Creissac Campos ; Santos,JA ; 5659 ; 5523 ; 5599