[seL4] adding new code to VMM on TK1