As part of my software engineering degree at UNSW I had to do a year-long honours thesis. I ended up doing my thesis with the Trustworthy Systems group at UNSW (formerly Data61, and I happened to do my thesis as that was all happening).
The goal was to look into getting something similar to secure boot or TPM attestation working on an seL4-based system. Ultimately, it did result in a somewhat working implementation of TPM attestation. There wasn't much research value in this though. There's some interesting considerations in how the secure monitor calls should be handled in a formally verified system, but these were largely handled better by some concurrent work that was happening in the rest of the seL4 ecosystem. There are a few ideas towards the end of the thesis on how I think the same security principles could be implemented better with seL4.
The code for this is in a pretty bad state as I rushed to get everything working in time, so I haven't published any of it.