Ring 3 iopl is going away, seL4 is ok
Hello, I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me. Here's Intel's RFC: https://www.intel.com/content/www/us/en/developer/articles/technical/envisio... I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways! -- William ML Leslie
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On Sun, May 21, 2023 at 01:40:31PM +1000, William ML Leslie wrote:
Hello,
I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me.
Here's Intel's RFC:
https://www.intel.com/content/www/us/en/developer/articles/technical/envisio...
I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways!
(Off-topic) Where can I find information on Coyotos? What advantages does it have over seL4, and do you plan to formally verify it in the future? - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmRppQUACgkQsoi1X/+c IsE8gRAAtBwtqKmd2q8jXokvebHNXBe2Stm14twkVGUrSEZN2t6CVOjwI11rFdH8 WQ0x/sUfBvHNIw9ggq/taRYAawYm5EsgOskETco1Kz1oNnzPD/euS74PY0cEP/et q283mdFzg2utTDNnlur/ZKqRT+VRH6WYK8CORJBbqpMeuMg0joPkCty5gIzzQB7L y09bvXEYksvAbaZ2DAunJ1t2ldeVHBvhvvkGINHtosn2hxQ0xgAXnfF0xr5K/lh3 YHqVevgAUuLWYuYbdQjQ3cUmduBUwhNRWmpS7ktbEhF31xQm5lBIO8QjVqMLdulT LUp+EnmCY9s+Ua76eedlLXUQUiiZBVdqhHSrMIWYvTfwoxPr+z0X0pELjllmsFoq 0Kk+6I36KNRUNg9rcGpGlOFvh9fYzIcq3rI0EdWgadklvPr1TiYCdt+7dRb2JXWG kZnMdWHrkhu8GmTnk4QX+YqUmx/7+MfhcBY0+xe3wXkuBc4gRqUk64LDCnkECWkB oeEBz5mBlq/nTPCT0sVokUdeWEfmK2AVDYpiJ4Gkqv4Ny/0TY9AqHy8q+DVonZcM VKu+qJfJp2xuMOXgAl6EAPSCn85ukmzyCgmwwgLsyReTuDq8GTWM4wATwT9sDB+6 kEWl+UyODsJi/V16evD9mUBpKmYThfoOOLqPMDh7ZW0AyJcKlZU= =qhke -----END PGP SIGNATURE-----
On Sun, 21 May 2023 at 14:58, Demi Marie Obenour < demi@invisiblethingslab.com> wrote:
(Off-topic) Where can I find information on Coyotos? What advantages does it have over seL4, and do you plan to formally verify it in the future?
I maintain Coyotos and its toolchain on my gitlab, but so far it has been mostly maintenance rather than active development. I sometimes discuss progress and questions on the general cap-talk google group. I'm trying to use it as a test bed for things that could eventually make it into seL4, without having to hit a moving target or need to keep existing users happy. So, formal verification is at the very least out of reach for me at this point. I definitely recommend seL4 for production deployments, not only because of the better support and the verification, but also because the documentation is much higher quality. https://gitlab.com/william-ml-leslie/coyotos -- William ML Leslie
On 5/20/23, William ML Leslie
Hello,
I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me.
I'd actually thought of trying to add support for direct use of PMIO instructions in user code under seL4 at one point, but there's probably not much of a point in that because modern performance-critical devices most often use just MMIO only. Really I'm not sure why Intel wouldn't just do away with PMIO entirely and just map ports onto MMIO (like on non-x86 architectures with PCI-like buses) if they're trying to clean up legacy cruft. Another thing that would be an issue is the 32-bit boot code. I have preliminary code in my custom Multiboot loader for loading a 64-bit kernel directly into long mode, but I only ever used it with earlier experiments and never with seL4. I have disabled the ELF32 kernel conversion in my OS since my loader supports ELF64 binaries even though only 32-bit entry is working with seL4. Of course, my loader works rather differently than the CAmkES/seL4CP one does (the image is a list of separate Multiboot modules, one per file, rather than a cpio archive linked into the root server), so it wouldn't necessarily be a replacement.
participants (3)
-
Andrew Warkentin -
Demi Marie Obenour -
William ML Leslie