  @mastersthesis{Nair:bsc,
    address          = {Sydney, Australia},
    author           = {Sai Nair},
    keywords         = {L4v, time protection, micro-architectural timing channels, seL4, covert channels, isabelle/hol,
                        invariance proofs, refinement},
    month            = nov,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/25/Nair%3Absc.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Updating {L4v} Invariants to Aid Time Protection Proofs},
    type             = {{BSc(Hons)} Thesis},
    year             = {2025}
  }