This is a very small issue.
If I understand the L4 specifications correctly, typed words provided by the sender are copied to the recipient. This allows the recipient to know what was sent.
An observation:
The transfer of typed words exposes sender-side address values to the receiver. This is a small security violation, since there is no valid use that the receiver can make of this information. It is probably not an important issue, except that we noticed an interaction with cross-model calls.
If the IPC transport replaces these addresses with zero, it becomes possible to re-encode a 64-bit typed item word into a 32-bit typed item word without losing any useful information.
This appears (to us) to be useful in the implementation of IPCs that cross from (e.g.) 64-bit sender to 32-bit receiver.
It does not appear to us that the receiver loses any useful information if the sender address is zeroed or truncated. Have we missed something?
shap