Detecting noninterference violations with property-based testing

Andrade Guanoquiza, Fernanda Lucía (2023). Detecting noninterference violations with property-based testing. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).


Title: Detecting noninterference violations with property-based testing
  • Andrade Guanoquiza, Fernanda Lucía
Item Type: Thesis (Master thesis)
Masters title: Métodos Formales en Ingeniería Informática
Date: July 2023
Freetext Keywords: Software verification, property-based testing, information-flow control, noninterference
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[thumbnail of TFM_FERNANDA_ANDRADE_GUANOQUIZA.pdf] PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (535kB)


In today’s interconnected digital world, protecting sensitive data is critical. However, the design and verification of information-flow control (IFC) mechanisms, crucial for data security, present significant challenges. In this work, we propose the integration of property-based testing into the verification process of IFC mechanisms, utilizing the existing metatheory as a foundation.

Property-based testing can streamline the formal verification of information-flow control mechanisms by generating random test cases. This approach can expose errors early in the proving process, guiding users toward accurate design and implementation. By generating counterexamples, property-based testing can effectively uncover potential noninterference violations.

We illustrate the effectiveness of this approach by applying it to the DypLIO library, a Haskell-based IFC mechanism designed to enforce security policies. This application successfully identified issues in both the implementation and the ongoing proof mechanization. Our results highlight the potential of propertybased testing as a complementary strategy for enhancing the security of IFC mechanisms.

More information

Item ID: 75865
DC Identifier:
OAI Identifier:
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 14 Sep 2023 10:49
Last Modified: 14 Sep 2023 10:53
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM