Search results for:

Filter your results

0 Search results

High-Assurance Software

About the Centre

At the High-Assurance Software Laboratory (HASLab), we improve practice through theory, creating and implementing software that goes beyond mere functionality: we ensure it is correct, resilient, and secure against failures and attacks.

Our team of researchers, scientists, and engineers has proven expertise in software engineering, developing methods and tools to design and integrate robust software; in distributed systems, exploring distribution and replication to ensure scalability and reliability; and in information security, addressing cybersecurity challenges and improving systems with advanced, secure cryptographic protocols, thus minimising vulnerabilities.

With a multidisciplinary approach supported by solid theoretical principles, we develop innovative solutions for critical software, secure cloud infrastructures, and privacy-aware big data management, driving scientific advancement, innovation, and high-level consultancy.

In addition, we complement our core expertise with work in human-computer interaction, programming languages, computational mathematics, and quantum computing - because we believe the future of trustworthy software is built on knowledge and innovation.

Centre Areas

Information Security

Our research in Information Security combines rigorous theoretical foundations with innovative practical approaches. We aim to build secure systems with formal guarantees, bridging the development of cryptographic protocols with their efficient and reliable implementation. On the theoretical side, we work with security proofs and computer-assisted cryptography, developing formal techniques that automatically validate security properties. On the applied side, we focus on implementations that meet high standards of performance and security, ensuring that theoretical guarantees are preserved from specification through to final code. To achieve this, we design domain-specific languages and tools that facilitate the development of highly trustworthy cryptographic software. We also investigate advanced threat detection and response mechanisms, which are essential to continuously preserving the security properties of systems. Our solutions are applicable to several domains, including privacy-preserving technologies, secure data storage, and cloud computing — all critical areas for ensuring security in the digital age.

Distributed Systems

In Distributed Systems, we are transforming the way data is managed in cloud computing, critical systems, advanced computing infrastructures, and artificial intelligence ecosystems. We explore new frontiers in reliability, replication, and data distribution, developing novel consensus protocols and conflict-free approaches to eventual consistency, ensuring data integrity through replicated data types. We optimise the processing of transactional and analytical workloads in databases and create secure methods for handling data in untrusted environments, enhancing the resilience and security of systems. Learn more here. We design efficient data storage solutions capable of keeping up with the rapid growth of digital information. We use modern technologies to meet the demands for performance, scalability, reliability, security, and energy efficiency. Discover more here. We develop middleware systems with a focus on semantic interoperability, applied to real-world use cases and data spaces. Our mission is to shape the future of distributed data management, with solutions for the next generation of digital services.

Software Engineering

In our Software Engineering research, we aim to transform system development by making it more secure, efficient, and sustainable. To achieve this, we apply rigorous approaches to ensure software quality—from design to implementation—using formal guarantees to ensure correct system behaviour. Learn more here. We explore new ways to make systems more sustainable and to optimise complex processes, including those involving large-scale data or computation, reducing resource requirements and improving energy efficiency. Our work also addresses user interaction, designing more intuitive and accessible interfaces that ensure a smooth and effective user experience. We also investigate the potential of quantum computing in software engineering, studying how it can be integrated to create faster more secure systems that are equipped to tackle complex challenges. In doing so, we contribute to a more responsible and innovative digital future, ready to meet the challenges of tomorrow.

Flagship Projects

PeT

EPICURE

Team Members

Team Leaders

António Luís Sousa

Centre Coordinator

Catarina Leones Fernandes

Assistant to the Centre Coordinator

Team Members

Adriano Novo Maior

Researcher

Alcino Cunha

Research Coordinator

Alexandra Sofia Mendes

Senior Researcher

Alexandre Almeida Filho

Alexandre Rodrigues Fernandes

Alexis Gonzalez

Alícia Oliveira

Researcher

Álvaro Festas Silva

Ana Isabel Neri

Ana Nunes Alonso

Assistant Researcher

Ana Rita Guimarães

André de Sousa

André Lucena Ferreira

André Manuel Sequeira

Assistant Researcher

André Martins Pereira

Senior Researcher

Selected Publications

Formally Verifying Kyber Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt

Almeida, JB;Olmos, SA;Barbosa, M;Barthe, G;Dupressoir, F;Grégoire, B;Laporte, V;Lechenet, JC;Low, C;Oliveira, T;Pacheco, H;Quaresma, M;Schwabe, P;Strub, PY;

2024

ADVANCES IN CRYPTOLOGY - CRYPTO 2024, PT II