Αποστολή με SMS: Formal Models of Operating System Kernels