Fernanda Andrade

VP of Engineering at Stack Builders

I lead the development team at Stack Builders. In recent years, I have specialized in the use of functional languages for web application development. During this time, both I and my team at Stack Builders have explored how to make complex software more correct and manageable with functional programming and static types. This motivation also led me to delve deeper into the use of formal methods in the industry. I studied formal methods at UPM.

Detecting Noninterference Violations with Property-Based Testing

OBJECTIVES

- Present a program generation strategy by leveraging existing metatheory as the basis for generating lambda terms. 
- Demonstrate the benefits of integrating property-based testing into the verification process of IFC mechanisms, specifically for finding counterexamples of noninterference violations.

AUDIENCE

Researchers and programmers interested in metatheory and property-based testing

DESCRIPTION

In today’s digital world, safeguarding sensitive data is crucial. Yet, the verification of information-flow control (IFC) mechanisms, vital for data security, poses challenges. This talk explores how we can streamline the verification of IFC mechanisms by incorporating property-based testing. This involves generating random lambda terms to test the functionality of IFC mechanisms. The advantage of this approach is that it helps identify errors early in the verification process.

By generating counterexamples, property-based testing becomes a powerful tool for uncovering potential noninterference violations in the IFC mechanisms. To showcase its effectiveness, we applied this approach to an IFC library written in Haskell, currently being mechanized with Liquid Haskell. The results reveal issues in both the implementation and the ongoing proof mechanization, highlighting how property-based testing can be a complementary strategy for enhancing the security of IFC mechanisms.

←Back