HASLab - Other Publications

Permanent URI for this collection

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

Browse

Browsing HASLab - Other Publications by Title

  • Item
    Approaches to Conflict-free Replicated Data Types
    ( 2023) Paulo Sérgio Almeida ; 5607
  • Item
    Automated theorem proving for the systematic analysis of an infusion pump
    ( 2013) Michael Douglas Harrison ; Paolo Masci ; José Creissac Campos ; Curzon,P
  • Item
  • Item
  • Item
  • Item
  • 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
  • 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
  • Item
    Continuity as a computational effect
    ( 2015) Renato Jorge Neves ; Martins,ManuelA. ; Luís Soares Barbosa ; Hofmann,Dirk
  • 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
    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
    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
    Distance Perception in Immersive Environments - The Role of Photorealism
    ( 2015) Silva,C ; José Creissac Campos ; Santos,J ; Basso,D ; Mouta,S ; 5599
  • Item
    The dynamics of remembering and forgetting
    ( 2022) Carlos Baquero ; Cabecinhas,R ; 5596
  • Item
    Efficient State-based CRDTs by Delta-Mutation
    ( 2014) Paulo Sérgio Almeida ; Ali Shoker ; Carlos Baquero
  • Item
    Eventually Consistent Register Revisited
    ( 2015) Zawirski,M ; Carlos Baquero ; Bieniusa,A ; Preguiça,NM ; Shapiro,M
  • 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
    A Feature-based Classification of Model Repair Approaches
    ( 2015) Nuno Moreira Macedo ; Tiago,J ; Alcino Cunha