FLAT: Formal Languages as Types

Overview

FLAT proposes a type system approach that treats formal languages as first-class types in programming languages to distinguish between conceptually different string encodings. Conventional type systems conflate semantically distinct string types such as file paths, URLs, and email addresses under a single string type, creating opportunities for type-related vulnerabilities. The approach leverages context-free grammars and optional semantic constraints to restrict valid string values at the type level, enabling comprehensive solutions for documentation, validation, anomaly detection, and test generation.

Methods and approach

The FLAT framework uses context-free grammars as type definitions to enforce syntactic validity of strings. Semantic constraints can be layered atop grammatical restrictions for additional validation requirements. FLAT-PY instantiates this approach for Python through code instrumentation that performs runtime type checking on annotated code. Users annotate Python functions with formal language types and optional preconditions and postconditions. The instrumentation mechanism intercepts function calls and validates input and output strings against their declared types, reporting violations immediately upon detection.

Key Findings

Case studies on real Python code fragments demonstrate that FLAT-PY can detect logical bugs when combined with language-based fuzzing. The detection capability depends on an appropriate level of user annotation density. Runtime checking via instrumentation successfully identifies type mismatches between actual and expected string encodings, validating the practical utility of the approach for automated bug discovery.

Implications

Applying formal language types to strings addresses a fundamental gap in mainstream programming language type systems, where syntactic and semantic distinctions in string data are not captured. The integration of formal languages as types creates a foundation for multiple downstream applications including API documentation clarity, input validation automation, security vulnerability detection, fuzzing heuristics, and test oracle generation without requiring separate implementations.