Language-based Technology for Security - Homework 1

Master's Degree in Cybersecurity @ University of Pisa

Project Overview

This project implements a trusted interpreter for a functional programming language designed to protect software execution from untrusted code. The core objective is to provide a linguistic framework where trusted code and sensitive data can be isolated, while allowing the controlled invocation of trusted functions and the execution of external plugins.

To enforce security and prevent the leakage of sensitive information, the execution engine employs Dynamic Taint Analysis. This mechanism tracks the flow of "tainted" data (data originating from untrusted sources) and ensures that such data does not compromise the integrity of trusted blocks or lead to the unauthorized release of private information.

Key Security Features

• Trust Blocks: Specialized blocks used to group trusted functions and data.
• Confidentiality Levels: Support for Private (secret) and Public data to model access control.
• Handled Interfaces: A mechanism to explicitly define which functions within a trust block are exposed to the external environment.
• Plugin Management: Primitives to include and execute external code, with automatic taint assignment for untrusted plugins.
• Taint Tracking: Runtime monitoring of data flow to prevent sensitive data from leaking outside trust boundaries.

System Architecture

The project is developed in OCaml and organized using the Dune build system. The source code is located in the main/ directory.

Directory Structure

• main/
  • bin/: Contains the main entry point for running the interpreter with predefined test cases.
  • lib/: Contains the core implementation of the language.
  • test/: Contains the unit test suite.
  • dune-project: Dune project configuration.

Module Descriptions

• ast.ml: Defines the Abstract Syntax Tree (AST) for the language. It includes definitions for security levels (trust), confidentiality levels (confidentiality), and the expr type which encompasses all language constructs (e.g., Trust, Include, Execute, Handle).
• env.ml: Implements the environment management system, providing functions for binding variables and performing lookups.
• interpreter.ml: The heart of the project. It implements the eval function, which recursively evaluates expressions and enforces security policies, manages the taint status of values, and handles the transitions between trusted and untrusted contexts.
• utils.ml: Provides auxiliary helper functions used across the interpreter and tests.

Installation and Usage

Prerequisites

• OCaml: The OCaml compiler.
• Dune: The build system for OCaml.
• OUnit: For running the test suite.

Building the Project

To compile the project, navigate to the main/ directory and run:

cd main
dune build

Running the Project

To execute the main demonstration program:

dune exec bin/main.ml

To run the comprehensive unit test suite:

dune exec test/test_main.ml

Design Choices Summary

The implementation focuses on a strict separation between security levels. The use of an algebraic data type for expr allows for a clean mapping between the language specification and the interpreter's pattern-matching logic. Taint analysis is integrated directly into the evaluation process, ensuring that every operation on a value updates its taint status according to the security level of the surrounding context.