Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
    Factos & Números
    000
    Apresentação

    Laboratório de Software Confiável

    O HASLab dedica-se à criação e à implementação de sistemas de software confiável, i.e., software correto e resiliente perante falhas e ataques.

    De forma a cumprir este grande objetivo, o HASLab opera em três grandes áreas - Cibersegurança, Sistemas Distribuídos e Engenharia de Software.

    Engenharia de Software - são explorados métodos, técnicas e ferramentas para o desenvolvimento de software, podendo este ser integrado nas funcionalidades internas de determinados componentes, na sua configuração junto de outros componentes, e também na interação com o utilizador.

    Sistemas Distribuídos - com vista a melhorar a confiabilidade e a escalabilidade de software, explorando as propriedades inerentes à distribuição e à replicação de sistemas computacionais.

    Cibersegurança - de forma a minimizar a vulnerabilidade dos componentes de software a ataques, com recurso à implementação de estruturas e de protocolos criptográficos com propriedades de segurança formalmente comprovadas.

    Através de uma abordagem multidisciplinar que assenta em princípios teóricos comprovados, o HASLab visa disponibilizar soluções - fundamentos teóricos, métodos, linguagens, ferramentas - para o desenvolvimento de sistemas TIC abrangentes, dando garantias aos seus proprietários e utilizadores. Os grandes domínios de aplicação da investigação desenvolvida no HASLab incluem o desenvolvimento de sistemas de software cruciais para garantir a segurança e a proteção, a operacionalização de infraestruturas da nuvem seguras, e a gestão e o tratamento de big data, tendo em conta as questões da privacidade.

    Últimas Notícias

    Investigadores INESC TEC distinguidos com Bolsa de Mérito da UMinho

    Francisco Ribeiro e Michael Oliveira, investigadores do Laboratório de Software Confiável (HASLab) do INESC TEC, receberam a Bolsa de Mérito da UMinho pelo ano académico anterior. 

    21 junho 2019

    Novo membro na coordenação do HASLab

    Na reunião de Conselho de Administração do INESC TEC, que aconteceu no dia 7 de maio, foi comunicada a nomeação de António Luís Sousa para a co-coordenação do Laboratório de Software Confiável (HASLab), funções que exercerá em conjunto com Alcino Cunha, que se mantém como co-coordenador do Centro.

    17 junho 2019

    Terminou projeto que potencia criação de apps empresariais com dados não-relacionais

    RADicalize BigData, um projeto de prestação de serviços com a OutSystems, levado a cabo pelo Laboratório de Software Confiável (HASLab) do INESC TEC, permitiu desenvolver uma forma de integrar dados de fontes Big Data em aplicações empresariais usando uma abordagem low-code, compatível com a plataforma OutSystems.

    14 junho 2019

    A mais recente spin-off do INESC TEC chama-se Keyruptive

    A mais recente spin-off do INESC TEC chama-se Keyruptive e atua na área da segurança informática. Nasceu em Braga, fruto do trabalho de vários anos de um grupo de investigadores do Laboratório de Software Confiável (HASLab) do INESC TEC, e já tem uma solução tecnológica para apresentar ao mercado, cujo nome é igual ao da empresa agora criada.

    13 junho 2019

    INESC TEC lidera projeto europeu de 36M€ para digitalização do sistema elétrico

    O maior projeto colaborativo europeu aprovado pela Comissão Europeia, ao abrigo do programa de financiamento Horizonte 2020, chama-se InterConnect e vai ser liderado pelo INESC TEC.

    04 junho 2019

    Ver todas as Notícias
    004

    Projetos Selecionados

    DisaggregatedHPC

    Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

    2025-2026

    InfraGov

    InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

    2025-2026

    ENSCOMP4

    Ensino de Ciência da Computação nas Escolas 4

    2024-2025

    PFAI4_5eD

    Programa de Formação Avançada Industria 4 - 5a edição

    2024-2024

    Equipa
    Alcino Cunha

    Coordenador de Centro

    António Luís Sousa

    Coordenador de Centro

    Catarina Leones Fernandes

    Adjunto da Coordenação de Centro

    ViewClose Alphabet
    • a
    • b
    • c
    • d
    • e
    • f
    • g
    • h
    • i
    • j
    • k
    • l
    • m
    • n
    • o
    • p
    • q
    • r
    • s
    • t
    • u
    • v
    • w
    • x
    • y
    • z
    001

    Laboratório

    CLOUDinha

    Publicações

    HASLab Publicações

    Ler todas as publicações

    2024

    X-Wing

    Autores
    Barbosa, M; Connolly, D; Duarte, J; Kaiser, A; Schwabe, P; Varner, K; Westerbaan, B;

    Publicação
    IACR Communications in Cryptology

    Abstract
    X-Wing is a hybrid key-encapsulation mechanism based on X25519 and ML-KEM-768. It is designed to be the sensible choice for most applications. The concrete choice of X25519 and ML-KEM-768 allows X-Wing to achieve improved efficiency compared to using a generic KEM combiner. In this paper, we introduce the X-Wing hybrid KEM construction and provide a proof of security. We show (1) that X-Wing is a classically IND-CCA secure KEM if the strong Diffie-Hellman assumption holds in the X25519 nominal group, and (2) that X-Wing is a post-quantum IND-CCA secure KEM if ML-KEM-768 is itself an IND-CCA secure KEM and SHA3-256 is secure when used as a pseudorandom function. The first result is proved in the ROM, whereas the second one holds in the standard model. Loosely speaking, this means X-Wing is secure if either X25519 or ML-KEM-768 is secure. We stress that these security guarantees and optimizations are only possible due to the concrete choices that were made, and it may not apply in the general case.

    FecharLer Abstract

    2024

    Bare PAKE: Universally Composable Key Exchange from Just Passwords

    Autores
    Barbosa, M; Gellert, K; Hesse, J; Jarecki, S;

    Publicação
    ADVANCES IN CRYPTOLOGY - CRYPTO 2024, PT II

    Abstract
    In the past three decades, an impressive body of knowledge has been built around secure and private password authentication. In particular, secure password-authenticated key exchange (PAKE) protocols require only minimal overhead over a classical Diffie-Hellman key exchange. PAKEs are also known to fulfill strong composable security guarantees that capture many password-specific concerns such as password correlations or password mistyping, to name only a few. However, to enjoy both round-optimality and strong security, applications of PAKE protocols must provide unique session and participant identifiers. If such identifiers are not readily available, they must be agreed upon at the cost of additional communication flows, a fact which has been met with incomprehension among practitioners, and which hindered the adoption of provably secure password authentication in practice. In this work, we resolve this issue by proposing a new paradigm for truly password-only yet securely composable PAKE, called bare PAKE. We formally prove that two prominent PAKE protocols, namely CPace and EKE, can be cast as bare PAKEs and hence do not require pre-agreement of anything else than a password. Our bare PAKE modeling further allows to investigate a novel reusability property of PAKEs, i.e., whether n(2) pairwise keys can be exchanged from only n messages, just as the Diffie-Hellman non-interactive key exchange can do in a public-key setting. As a side contribution, this add-on property of bare PAKEs leads us to observe that some previous PAKE constructions relied on unnecessarily strong, reusable building blocks. By showing that non-reusable tools suffice for standard PAKE, we open a new path towards round-optimal post-quantum secure password-authenticated key exchange.

    FecharLer Abstract

    2024

    X-Wing: The Hybrid KEM You've Been Looking For

    Autores
    Barbosa, M; Connolly, D; Duarte, JD; Kaiser, A; Schwabe, P; Varner, K; Westerbaan, B;

    Publicação
    IACR Cryptol. ePrint Arch.

    Abstract

    Ler Publicação Completa

    2024

    A Tight Security Proof for SPHINCS+, Formally Verified

    Autores
    Barbosa, M; Dupressoir, F; Hülsing, A; Meijers, M; Strub, PY;

    Publicação
    Advances in Cryptology - ASIACRYPT 2024 - 30th International Conference on the Theory and Application of Cryptology and Information Security, Kolkata, India, December 9-13, 2024, Proceedings, Part IV

    Abstract

    2023

    TADA: A Toolkit for Approximate Distributed Agreement

    Autores
    da Conceiçao, EL; Alonso, AN; Oliveira, RC; Pereira, JO;

    Publicação
    DISTRIBUTED APPLICATIONS AND INTEROPERABLE SYSTEMS, DAIS 2023

    Abstract
    Approximate agreement has long been relegated to the sidelines compared to exact consensus, with its most notable application being clock synchronisation. Other proposed applications stemming from control theory target multi-agent consensus, namely for sensor stabilisation, coordination in robotics, and trust estimation. Several proposals for approximate agreement follow the Mean Subsequence Reduce approach, simply applying different functions at each phase. However, taking clock synchronisation as an example, applications do not fit neatly into the MSR model: Instead they require adapting the algorithms' internals. Our contribution is two-fold. First, we identify additional configuration points, establishing a more general template of MSR approximate agreement algorithms. We then show how this allows us to implement not only generic algorithms but also those tailored for specific purposes (clock synchronisation). Second, we propose a toolkit for making approximate agreement practical, providing classical implementations as well as allow these to be configured for specific purposes. We validate the implementation with classical algorithms and clock synchronisation.

    FecharLer Abstract

    Factos & Números

    16Docentes do Ensino Superior

    2020

    4Artigos em revistas indexadas

    2020

    0Capítulos de livros

    2020

    Ver todos os Factos & Números
    Contactos
    António Luís Sousa

    -

    +351253604440

    antonio.l.sousa@inesctec.pt

    Alcino Cunha

    Coordenado de Centro

    +351253604440

    alcino.cunha@inesctec.pt