diff --git a/Cargo.lock b/Cargo.lock
index 9f207db8e..e66c98d46 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2277,6 +2277,20 @@ dependencies = [
  "serde_json",
 ]
 
+[[package]]
+name = "sel4-hal-adapters"
+version = "0.1.0"
+dependencies = [
+ "log",
+ "sel4-bounce-buffer-allocator",
+ "sel4-externally-shared",
+ "sel4-microkit",
+ "sel4-microkit-message",
+ "sel4-shared-ring-buffer",
+ "serde",
+ "smoltcp",
+]
+
 [[package]]
 name = "sel4-immediate-sync-once-cell"
 version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
index a649a769f..a691a051f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -86,6 +86,7 @@ members = [
     "crates/sel4-dlmalloc",
     "crates/sel4-externally-shared",
     "crates/sel4-generate-target-specs",
+    "crates/sel4-hal-adapters",
     "crates/sel4-immediate-sync-once-cell",
     "crates/sel4-immutable-cell",
     "crates/sel4-initialize-tls-on-stack",
diff --git a/crates/sel4-hal-adapters/Cargo.nix b/crates/sel4-hal-adapters/Cargo.nix
new file mode 100644
index 000000000..77eda0996
--- /dev/null
+++ b/crates/sel4-hal-adapters/Cargo.nix
@@ -0,0 +1,31 @@
+{ mk, versions, localCrates, smoltcpWith, serdeWith, authors }:
+
+mk {
+  package.name = "sel4-hal-adapters";
+  package.authors = with authors; [
+    nspin
+    "Ben Hamlin <hamlinb@galois.com>"
+  ];
+  dependencies = {
+    inherit (versions) log;
+    smoltcp = smoltcpWith [] // { optional = true; };
+    serde = serdeWith [];
+  } // (with localCrates; {
+    inherit sel4-microkit-message;
+    sel4-microkit = sel4-microkit // { default-features = false; };
+
+    # smoltcp-phy deps
+    sel4-bounce-buffer-allocator = sel4-bounce-buffer-allocator // { optional = true; };
+    sel4-externally-shared = sel4-externally-shared // { optional = true; features = ["unstable"]; };
+    sel4-shared-ring-buffer = sel4-shared-ring-buffer // { optional = true; };
+  });
+  features = {
+    default = ["smoltcp-hal"];
+    smoltcp-hal = [
+      "smoltcp"
+      "sel4-shared-ring-buffer"
+      "sel4-externally-shared"
+      "sel4-bounce-buffer-allocator"
+    ];
+  };
+}
diff --git a/crates/sel4-hal-adapters/Cargo.toml b/crates/sel4-hal-adapters/Cargo.toml
new file mode 100644
index 000000000..2f5357367
--- /dev/null
+++ b/crates/sel4-hal-adapters/Cargo.toml
@@ -0,0 +1,45 @@
+#
+# Copyright 2023, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+#
+# This file is generated from './Cargo.nix'. You can edit this file directly
+# if you are not using this project's Cargo manifest management tools.
+# See 'hacking/cargo-manifest-management/README.md' for more information.
+#
+
+[package]
+name = "sel4-hal-adapters"
+version = "0.1.0"
+authors = ["Nick Spinale <nick.spinale@coliasgroup.com>", "Ben Hamlin <hamlinb@galois.com>"]
+edition = "2021"
+license = "BSD-2-Clause"
+
+[features]
+default = ["smoltcp-hal"]
+smoltcp-hal = [
+    "smoltcp",
+    "sel4-shared-ring-buffer",
+    "sel4-externally-shared",
+    "sel4-bounce-buffer-allocator",
+]
+
+[dependencies]
+log = "0.4.17"
+sel4-bounce-buffer-allocator = { path = "../sel4-bounce-buffer-allocator", optional = true }
+sel4-microkit = { path = "../sel4-microkit", default-features = false }
+sel4-microkit-message = { path = "../sel4-microkit/message" }
+sel4-shared-ring-buffer = { path = "../sel4-shared-ring-buffer", optional = true }
+serde = { version = "1.0.147", default-features = false }
+
+[dependencies.sel4-externally-shared]
+path = "../sel4-externally-shared"
+features = ["unstable"]
+optional = true
+
+[dependencies.smoltcp]
+version = "0.10.0"
+default-features = false
+features = ["proto-ipv4", "proto-dhcpv4", "proto-dns", "socket-dhcpv4", "socket-dns", "socket-tcp"]
+optional = true
diff --git a/crates/sel4-hal-adapters/src/embedded_hal/mod.rs b/crates/sel4-hal-adapters/src/embedded_hal/mod.rs
new file mode 100644
index 000000000..9b4395aae
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/embedded_hal/mod.rs
@@ -0,0 +1,239 @@
+#![no_std]
+
+use num_enum::{IntoPrimitive, TryFromPrimitive};
+use zerocopy::{AsBytes, FromBytes};
+use core::fmt;
+use heapless::Deque;
+
+use embedded_hal::serial;
+use embedded_hal::prelude::_embedded_hal_serial_Write;
+use sel4cp::{Channel, Handler};
+use sel4cp::message::{MessageInfo, NoMessageValue, StatusMessageLabel};
+use sel4cp::message::MessageInfoRecvError;
+
+/// Handle messages using an implementor of [serial::Read<u8>] and [serial::Write<u8>].
+#[derive(Clone, Debug)]
+pub struct SerialHandler<Device, const READ_BUF_SIZE: usize = 256> {
+    /// Device implementing [serial::Read<u8>] and [serial::Write<u8>].
+    device: Device,
+    /// Channel for this component.
+    serial: Channel,
+    /// Channel for client component.
+    client: Channel,
+    /// Read buffer.
+    buffer: Deque<u8, READ_BUF_SIZE>,
+    /// Whether to notify client.
+    notify: bool,
+}
+
+impl<Device> SerialHandler<Device>
+where
+    Device: serial::Read<u8> + serial::Write<u8> + IrqDevice
+{
+    pub fn new(device: Device, serial: Channel, client: Channel) -> Self {
+        Self {
+            device,
+            serial,
+            client,
+            buffer: Deque::new(),
+            notify: true,
+        }
+    }
+}
+
+pub trait IrqDevice {
+    fn handle_irq(&self);
+}
+
+#[non_exhaustive]
+#[derive(Clone, Debug)]
+pub enum SerialHandlerError<Device>
+where
+    Device: serial::Read<u8> + serial::Write<u8>,
+    <Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone,
+    <Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone,
+{
+    ReadError(<Device as serial::Read<u8>>::Error),
+    WriteError(<Device as serial::Write<u8>>::Error),
+    BufferFull,
+    // XXX Other errors?
+}
+
+impl<Device> fmt::Display for SerialHandlerError<Device>
+where
+    Device: serial::Read<u8> + serial::Write<u8>,
+    <Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone,
+    <Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone,
+{
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match *self {
+            SerialHandlerError::ReadError(_) => write!(f, "SerialHandlerError::ReadError"),
+            SerialHandlerError::WriteError(_) => write!(f, "SerialHandlerError::WriteError"),
+            SerialHandlerError::BufferFull => write!(f, "SerialHandlerError::BufferFull"),
+        }
+    }
+}
+
+impl<Device> Handler for SerialHandler<Device>
+where
+    Device: serial::Read<u8> + serial::Write<u8> + IrqDevice,
+    <Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone,
+    <Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone,
+{
+    type Error = SerialHandlerError<Device>;
+
+    fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> {
+        // TODO Handle errors
+        if channel == self.serial {
+            while let Ok(c) = self.device.read() {
+                if let Err(_) = self.buffer.push_back(c) {
+                    return Err(SerialHandlerError::BufferFull);
+                }
+            }
+            self.device.handle_irq();
+            self.serial.irq_ack().unwrap();
+            if self.notify {
+                self.client.notify();
+                self.notify = false;
+            }
+        } else {
+            unreachable!() // XXX Is this actually unreachable?
+        }
+        Ok(())
+    }
+
+    fn protected(
+        &mut self,
+        channel: Channel,
+        msg_info: MessageInfo,
+    ) -> Result<MessageInfo, Self::Error> {
+        // TODO Handle errors
+        if channel == self.client {
+            match msg_info.label().try_into().ok() /* XXX Handle errors? */ {
+                Some(RequestTag::Write) => match msg_info.recv() {
+                    Ok(WriteRequest { val }) => {
+                        // Blocking write
+                        while let Err(nb::Error::WouldBlock) = self.device.write(val) {}
+                        Ok(MessageInfo::send(StatusMessageLabel::Ok, NoMessageValue))
+                    }
+                    Err(_) => Ok(MessageInfo::send(StatusMessageLabel::Error, NoMessageValue)),
+                },
+                Some(RequestTag::Read) => match self.buffer.pop_front() {
+                    Some(val) => {
+                        Ok(MessageInfo::send(ReadResponseTag::Some, ReadSomeResponse { val }))
+                    }
+                    None => {
+                        self.notify = true;
+                        Ok(MessageInfo::send(ReadResponseTag::None, NoMessageValue))
+                    }
+                },
+                None => Ok(MessageInfo::send(StatusMessageLabel::Error, NoMessageValue)),
+            }
+        } else {
+            unreachable!() // XXX Is this actually unreachable?
+        }
+    }
+}
+
+/// Device-independent embedded_hal::serial interface to a serial-device
+/// component. Interact with it using [serial::Read], [serial::Write],
+/// and [fmt::Write].
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SerialDriver {
+    pub channel: Channel
+}
+
+impl SerialDriver {
+    pub fn new(channel: Channel) -> Self {
+        SerialDriver { channel }
+    }
+}
+
+#[derive(Clone, Debug)]
+pub enum ReadError {
+    RecvError(MessageInfoRecvError),
+    InvalidResponse,
+    EOF,
+}
+
+impl serial::Read<u8> for SerialDriver {
+    type Error = ReadError;
+
+    // XXX Unclear if this blocks or how to prevent it from doing so...
+    fn read(&mut self) -> nb::Result<u8, Self::Error> {
+        let msg_info = self.channel
+            .pp_call(MessageInfo::send(RequestTag::Read, NoMessageValue));
+
+        match msg_info.label().try_into() {
+            Ok(ReadResponseTag::Some) => match msg_info.recv() {
+                Ok(ReadSomeResponse { val }) => Ok(val),
+                Err(e) => Err(nb::Error::Other(ReadError::RecvError(e))),
+            },
+            Ok(ReadResponseTag::None) => Err(nb::Error::Other(ReadError::EOF)),
+            Err(_) => Err(nb::Error::Other(ReadError::InvalidResponse)),
+        }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum WriteError {
+    SendError,
+    InvalidResponse,
+}
+
+impl serial::Write<u8> for SerialDriver {
+    type Error = WriteError;
+
+    // XXX Unclear if this blocks or how to prevent it from doing so...
+    fn write(&mut self, val: u8) -> nb::Result<(), Self::Error> {
+        let msg_info = self.channel
+            .pp_call(MessageInfo::send(RequestTag::Write, WriteRequest { val }));
+
+        match msg_info.label().try_into() {
+            Ok(StatusMessageLabel::Ok) => Ok(()),
+            Ok(StatusMessageLabel::Error) => Err(nb::Error::Other(WriteError::SendError)),
+            Err(_) => Err(nb::Error::Other(WriteError::InvalidResponse)),
+        }
+    }
+
+    fn flush(&mut self) -> nb::Result<(), Self::Error> {
+        todo!()
+    }
+}
+
+// XXX There's already an implementation of core::fmt::Write for serial::Write
+// in embedded_hal::fmt, but I'm not clear on how to use it.
+impl fmt::Write for SerialDriver {
+    fn write_str(&mut self, s: &str) -> fmt::Result {
+        s.as_bytes().iter().copied().for_each(|b| { let _ = self.write(b); });
+        Ok(())
+    }
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, IntoPrimitive, TryFromPrimitive)]
+#[cfg_attr(target_pointer_width = "32", repr(u32))]
+#[cfg_attr(target_pointer_width = "64", repr(u64))]
+pub enum RequestTag {
+    Write,
+    Read,
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, AsBytes, FromBytes)]
+#[repr(C)]
+pub struct WriteRequest {
+    pub val: u8,
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, IntoPrimitive, TryFromPrimitive)]
+#[cfg_attr(target_pointer_width = "32", repr(u32))]
+#[cfg_attr(target_pointer_width = "64", repr(u64))]
+pub enum ReadResponseTag {
+    None,
+    Some,
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, AsBytes, FromBytes)]
+#[repr(C)]
+pub struct ReadSomeResponse {
+    pub val: u8,
+}
diff --git a/crates/sel4-hal-adapters/src/lib.rs b/crates/sel4-hal-adapters/src/lib.rs
new file mode 100644
index 000000000..c94ba0047
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/lib.rs
@@ -0,0 +1,7 @@
+#![no_std]
+#![feature(never_type)]
+#![feature(strict_provenance)]
+#![feature(let_chains)]
+
+#[cfg(feature = "smoltcp-hal")]
+pub mod smoltcp;
diff --git a/crates/sel4-hal-adapters/src/smoltcp/mod.rs b/crates/sel4-hal-adapters/src/smoltcp/mod.rs
new file mode 100644
index 000000000..7416009ff
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/smoltcp/mod.rs
@@ -0,0 +1 @@
+pub mod phy;
diff --git a/crates/sel4-hal-adapters/src/smoltcp/phy/device.rs b/crates/sel4-hal-adapters/src/smoltcp/phy/device.rs
new file mode 100644
index 000000000..dd15237b7
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/smoltcp/phy/device.rs
@@ -0,0 +1,3 @@
+//! Client-side [`smoltcp::phy::Device`] implementation
+
+pub use sel4_shared_ring_buffer::*;
diff --git a/crates/sel4-hal-adapters/src/smoltcp/phy/handler.rs b/crates/sel4-hal-adapters/src/smoltcp/phy/handler.rs
new file mode 100644
index 000000000..e21fd9587
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/smoltcp/phy/handler.rs
@@ -0,0 +1,159 @@
+//! A generic microkit handler for implementors of [`smoltcp::phy::Device`].
+
+use smoltcp::{
+    phy::{self, RxToken, TxToken},
+    time::Instant,
+};
+
+use serde::{Deserialize, Serialize};
+
+use sel4_externally_shared::ExternallySharedRef;
+use sel4_microkit::{Channel, Handler, MessageInfo};
+use sel4_microkit_message::MessageInfoExt as _;
+use sel4_shared_ring_buffer::RingBuffers;
+
+pub trait IrqAck {
+    fn irq_ack(&mut self);
+}
+
+pub trait HasMac {
+    fn mac_address(&self) -> [u8; 6];
+}
+
+#[derive(Debug, Serialize, Deserialize)]
+pub struct MacAddress(pub [u8; 6]);
+
+#[derive(Debug, Serialize, Deserialize)]
+pub enum Request {
+    GetMacAddress,
+}
+
+#[derive(Debug, Serialize, Deserialize)]
+pub struct GetMacAddressResponse {
+    pub mac_address: MacAddress,
+}
+
+pub struct PhyDeviceHandler<Device> {
+    dev: Device,
+    client_region: ExternallySharedRef<'static, [u8]>,
+    client_region_paddr: usize,
+    rx_ring_buffers: RingBuffers<'static, fn() -> Result<(), !>>,
+    tx_ring_buffers: RingBuffers<'static, fn() -> Result<(), !>>,
+    device_channel: Channel,
+    client_channel: Channel,
+}
+
+impl<Device> PhyDeviceHandler<Device> {
+    pub fn new(
+        dev: Device,
+        client_region: ExternallySharedRef<'static, [u8]>,
+        client_region_paddr: usize,
+        rx_ring_buffers: RingBuffers<'static, fn() -> Result<(), !>>,
+        tx_ring_buffers: RingBuffers<'static, fn() -> Result<(), !>>,
+        device_channel: Channel,
+        client_channel: Channel,
+    ) -> Self {
+        // XXX We could maybe initialize DMA here, so we don't need to do
+        // it in main. Also maybe initialize the ring buffers.
+        Self {
+            dev,
+            client_region,
+            client_region_paddr,
+            rx_ring_buffers,
+            tx_ring_buffers,
+            device_channel,
+            client_channel,
+        }
+    }
+}
+
+impl<Device: phy::Device + IrqAck + HasMac> Handler for PhyDeviceHandler<Device> {
+    type Error = !;
+
+    fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> {
+        if channel == self.device_channel || channel == self.client_channel {
+            let mut notify_rx = false;
+
+            while !self.rx_ring_buffers.free().is_empty()
+                && let Some((rx_tok, _tx_tok)) = self.dev.receive(Instant::ZERO) {
+                    let desc = self.rx_ring_buffers.free_mut().dequeue().unwrap();
+                    let desc_len = usize::try_from(desc.len()).unwrap();
+
+                    rx_tok.consume(|rx_buf| {
+                        assert!(desc_len >= rx_buf.len());
+                        let buf_range = {
+                            let start = desc.encoded_addr() - self.client_region_paddr;
+                            start..start + rx_buf.len()
+                        };
+                        self.client_region
+                            .as_mut_ptr()
+                            .index(buf_range)
+                            .copy_from_slice(&rx_buf);
+                    });
+
+                    self.rx_ring_buffers.used_mut().enqueue(desc).unwrap();
+                    notify_rx = true;
+                }
+
+            if notify_rx {
+                self.rx_ring_buffers.notify().unwrap();
+            }
+
+            let mut notify_tx = false;
+
+            while !self.tx_ring_buffers.free().is_empty()
+                && let Some(tx_tok) = self.dev.transmit(Instant::ZERO) {
+                    let desc = self.tx_ring_buffers.free_mut().dequeue().unwrap();
+                    let tx_len = usize::try_from(desc.len()).unwrap();
+
+                    tx_tok.consume(tx_len, |tx_buf| {
+                        let buf_range = {
+                            let start = desc.encoded_addr() - self.client_region_paddr;
+                            start..start + tx_len
+                        };
+                        self.client_region
+                            .as_ptr()
+                            .index(buf_range)
+                            .copy_into_slice(tx_buf);
+                    });
+
+                    self.tx_ring_buffers.used_mut().enqueue(desc).unwrap();
+                    notify_tx = true;
+                }
+
+            if notify_tx {
+                self.tx_ring_buffers.notify().unwrap();
+            }
+
+            self.dev.irq_ack();
+            self.device_channel.irq_ack().unwrap();
+        } else {
+            unreachable!()
+        }
+
+        Ok(())
+    }
+
+    fn protected(
+        &mut self,
+        channel: Channel,
+        msg_info: MessageInfo,
+    ) -> Result<MessageInfo, Self::Error> {
+        Ok(if channel == self.client_channel {
+            match msg_info.recv_using_postcard::<Request>() {
+                Ok(req) => match req {
+                    Request::GetMacAddress => {
+                        let mac_address = self.dev.mac_address();
+                        MessageInfo::send_using_postcard(GetMacAddressResponse {
+                            mac_address: MacAddress(mac_address),
+                        })
+                        .unwrap()
+                    }
+                },
+                Err(_) => MessageInfo::send_unspecified_error(),
+            }
+        } else {
+            unreachable!()
+        })
+    }
+}
diff --git a/crates/sel4-hal-adapters/src/smoltcp/phy/mod.rs b/crates/sel4-hal-adapters/src/smoltcp/phy/mod.rs
new file mode 100644
index 000000000..9789e45c8
--- /dev/null
+++ b/crates/sel4-hal-adapters/src/smoltcp/phy/mod.rs
@@ -0,0 +1,5 @@
+mod handler;
+pub use handler::*;
+
+mod device;
+pub use device::*;