Where does the seL4 microkernel actually get the timing information it needs to enforce scheduling decisions?

I can imagine some sort of interrupt or I/O access is required to get it from the raw hardware.

How does it get from the timing hardware to the scheduling code?