September 2, 2026 · Alex Potanin

Making a Robot Arm Impossible to Misuse from Its Own Computer

Today we made a robot arm impossible to misuse from its own computer. Not “hard”. Impossible, in the sense that the software driving the motors can no longer reach them except through a gatekeeper it cannot see, cannot touch, and cannot switch off.

This is joint work between Fiducia and the seL4 Foundation community, here at the ANU School of Computing and UNSW Computer Science and Engineering — securing Embodied AI on robots, cars, drones, and other embedded devices.

The setup

A Unitree D1 arm runs Ubuntu on a small board. The manufacturer's control software talks to seven servos over a serial cable. Anyone with root on that Ubuntu — a bug, a bad motion plan, or an attacker — can command any joint anywhere: into the table, into a person, into itself.

What we did

We booted seL4 on that board instead, and ran the arm's own, unmodified Ubuntu inside it as a guest. The serial cable to the motors now belongs to a tiny separate program outside Linux. Every command Linux sends passes through a filter that knows the arm's geometry: it computes where the fingertips will end up and refuses anything that takes them below the table.

The demo is simple. Tell the arm to touch the desk. Under plain Ubuntu it does. Under seL4 it stops ten centimetres above, and a line appears on a console Linux cannot write to, explaining why.

The manufacturer's software runs exactly as before. Same binaries, same network address, same ssh, same web GUI. It does not know anything changed. Root inside it cannot change anything either, because the policy lives in a different address space and Linux holds no capability for the hardware. That is not a configuration setting. It is enforced by the memory management unit, under a kernel with a machine-checked proof that it enforces its access control.

Why not Docker, or a normal hypervisor?

• Containers are features of the same kernel that owns the hardware. Root or a kernel exploit steps around them. This arm ships a 2016-era vendor kernel that will never be patched.
• A Linux hypervisor has the right shape but puts a whole Linux host, millions of lines, in the path you are trying to protect.
• With seL4 the trusted part is the kernel plus about a thousand lines of filter and driver. It is the software equivalent of a separate safety microcontroller in the motor cable, on the same chip, retrofitted without touching the vendor's code or the robot's storage.

What it took

One engineer-day of hands-on bring-up on top of an offline-prepared system, seven power cycles, and a series of board-specific facts no generic driver knew: pin multiplexing, a bus-enable pin, an RS-485 direction line, parity and flow control left on by the bootloader. None of that was seL4 being hard. All of it was the reality of hardware, and all of it is now written down.

What it does not do

So you can trust the rest:

• The filter and drivers are ours, not verified;
• The geometry model is only as good as the URDF we fed it;
• It protects the servos, not the whole robot.

Those are exactly the things funding fixes.

Why this matters

This is the argument for investing in seL4 for robotics, medical devices and vehicles. The question is not whether your robot's Linux will be compromised. It is whether anything stands between that Linux and the motors when it is compromised. Today, for most robots, nothing does.

The work is open. If you build or buy robots or other devices and want this property in yours, talk to us.