Not a "bloated, monolithic system"?

Closer to rocket avionics. Part of it is running the intended code under test and verifying that all executed lines behave correctly with a coverage analyzer. Sometimes you can restrict scope by locking down the input and verifying only the parts of the shell that execute, other times you swap in a simpler shell to interpret the service management code and audit 100% of the simpler shell.

> Are you auditing algorithms and state machines to ensure all states and transitions are sane under any possible input?

Attack the problem the other way: precompute an execution plan for the service dependency graph, ordered and annotated for parallel execution. The service manager just executes that at runtime. Conceptually, "shell script" is close enough to get the idea across to people, and correct enough to use in prototyping, but it might be a compiled or interpreted representation of the shell script by the time it gets certified. Add a digital signature somewhere to verify it before executing it.

Most of the time the execution plan can be computed and verified by humans: you need storage, then start networking and UI in parallel, then your application runs until it crashes, then reboot. Someone checks that UI and networking do not in fact depend on each other. In more complicated cases you'd want a tool to do the ordering task, so you provide the auditors with evidence your tool is suitable for the way you use it.

The execution plan does not look anything like sysvinit scripts. It does not have all the capabilities of systemd, since the whole point is to avoid having to audit the parts of systemd you didn't use. Only the required functionality ends up on the target system.

Normally these do not change at runtime except in tightly constrained ways (e.g. a template service can have a variable number of children). If for some reason you need a crazy-high amount of flexibility at runtime in a certified system, there is theoretically a point where the complexity curves cross over and it's cheaper to just sit down and audit systemd.

> Are you auditing all input processing to make sure it can't result in buffer overflows or other sorts of security problems?

If auditing something like a shell, you get a report that says things like "can accept input lines up to the size of the RAM in the system, but don't do that, that would be bad" and "don't let random users control the input of the shell, that would be bad".

So the problem for the service manager script reduces to proving that the shell, as used for the specific service manager input in the specific service manager environment, behaves correctly. This can be as little as some light code review and coverage testing (plus a copy of the shell audit report and a checklist of all the restrictions you observed).

> Are your audits intended to ensure there's no leakage of personal information (eg in logs) that could run afoul of things like the GPDR?

It's never come up. The safety-critical systems don't have any personal information in them, and the security-critical ones have their own logging requirements that are out of scope of the service manager.

In some cases you can mix safety-critical and non-safety-critical services on a system provided there is appropriate isolation between them. Then you audit the safety-critical service, the service manager, and their dependencies, and mostly ignore the rest.