Formal validation of computational python

Python and Lean4 integrations, as structured docstrings, acts as a custom python3 wrapper / linter for CI/CD of computational mathematics and proofs that must hold for certain files, i.e. numpy could eventually use this to show their math library holds and eventually language equiveland, although this was a limitation as its not mathematically possible to show equivelance but it is possible to fluff test random values for each input as this is a formal verification tool between a functional and imperitive language which are inherintly incompadible.

The Problem

IPv4/IPv6 manipulation library ↗ mishandled leading-zero IPv4 strings, and this could allow access-control bypasses in applications relying on the library.

This was caused by a poor choice in design when the package was set up, but these kinds of issues are hard to see when you are tasked with writing a large library such as IPv4/IPv6. A tool like Lean4/Isabelle/COQ/Dafny would help mitigate manual issues by defining the roles of each theorem and what kinds of errors and inconsistencies they need to be able to detect.

The problem with that is that its not CI/CD verifiable, so any changes to a large library with many contributors could mean the wrong person edits the wrong files, that strictly and deterministically need to be correct.

My Role

This was a solo project, hence my role was programming the linter and lean4 ICP tool myself as there were no appropriate libraries already avaliable.

I did not submit or fix any issues with the IPv4/IPv6 library, I simply wrote a tool that they could have used to identify such an issue before it became a issue, and hopefully for future developers to find issues before they become a security vunerability.

The Solution & Process

The reason my project aligns with this problem was that IP addresses contain many really small theorems, usually one function per related theorem, and a tool that enforced correctness such as lean4 ↗ strictly attached and verified per theorem used in the code would be significant at finding issues such as the one above before they cause massive implications on any projects utilising such a tool, or when the tool eventually changes.

Example:

Failing Case

def _parse_octet(cls, octet_str):
    # PROBLEM: accepted and cast strings like "010" to decimal 10,
    octet_int = int(octet_str)
    
    if octet_int > 255:
        raise ValueError("Octet %d > 255" % octet_int)
    return octet_int

Passing Case

Note: the @Threorem block is how I specify lean4 theorems, the code below is a example, it is not completely correct as additional definitions would be required and probably wont make much sense unless you have used lean4 before.

@Theorem("""
def IsCanonicalOctet (s : String) : Prop :=
  s.length ≥ 1 ∧ 
  (s = "0" ∨ s.get ⟨0, ...⟩ ≠ '0') ∧ 
  ∀ c ∈ s, c ∈ "0123456789" ∧ 
  s.toNat ≤ 255

theorem bad_parser_correct :
    badParseOctet s = some n ↔
      IsCanonicalOctet s ∧ s.toNat = n := by
      ...
""") 
def _parse_octet(cls, octet_str):
    
    # where the Lean4 would identify a counterexample,
    # leading a developer to need to fix this function.
    # counterexample:
    #   s = "010"
    #   n = 10

    # FIX:
    if len(octet_str) > 1 and octet_str[0] == '0':
        raise ValueError("Leading zeros are not permitted")

    octet_int = int(octet_str)
    if octet_int > 255:
        raise ValueError("Octet %d > 255" % octet_int)
    return octet_int

How I built it?

I built this project with python

Technical Hurdles

key technical hurdles include