It's more like the focus has shifted from traditional OS kernels into virtualization, distributed systems and verification.
RE: seL4 borrows a lot of TrustedBSD (and to some extent Trusted Solaris). I don't know what the technical implementation details of Xen/XenServer are but once you add all the doo-dads, you've basically got VMware ESX with VMotion/HA/VSan in terms of functionality. I'll give VMware credit because VSan appliances are an easy-to-configure-and-deploy HA fairly-high-IOPS component of the VMware suite that's going to be a EMC SAN killer. The innovation there is how well it's integrated into the rest of the VMware virtual networking/vMotion/HA/disaster recovery suite, though, and not anything you could present at a conference.
I haven't looked at Mirage recently but I don't think they're doing anything really groundbreaking (i.e. academically; you won't see papers being presented on it)- a clever unikernel and useful tool but certainly not research. Read the old IBM Redbooks for z/OS and there's are numerous common components between the 1980s implementation of a System/390 running a hypervisor and and the Xen/ESX internals. I can only comment on IBM's stuff with confidence as a former IBMer, but VAX/VMS' clustering probably shares a lot of of what ESX is doing.
Other than IBM and MSR, a heavy funder of SPJ at Haskell and F# support as a primary language, definitely paid for itself many times over w/r/t language research the Python 3.5 async await syntax-sugar and, to some extent semantics, which was influenced by C# clearly, derived from F#2. Apple has a few people working on Clang (though not LLVM IIRC, so eh). Facebook has a really interesting language agnostic suite of analysis (primarily static) which I'm tracking carefully because it looks like it has a boatload of interesting capabilities.
There's a lot of interesting research going on, but not much of it is done by corporations, Microsoft Research notwithstanding.