Eric-Edlund
commented
1 year ago Improvements to message safety in #43 force modules to send from a privately held mailbox containing the module's id. This forces all sent messages to have the correct origin address.
All messages now have a universally unique type and the message system filters messages before they're sent so that modules only ever receive message types they have declared they may receive.
Message_Record is now an immutable object and it has been made much more difficult for module writers to tamper with messages directly.
There is no compile time enforcement to verify that messages are sent to the correct mailbox. This means that modules need to defend themselves against the possibility of receiving inappropriate messages, increasing overhead and reducing static reliability. It would be nice to have a tool that verifies that all messages sent to a mailbox were generated using the corresponding module's API encoder functions. To do this would require some flow analysis of the client code to determine where messages are being created and to verify that they aren't being modified in some way after they are constructed. Could SPARK's analysis be used to do this in some way?
Note that this is a different issue from verifying that there is a proper one-to-one correspondence between modules and mailboxes. Even with such a correspondence in place it would still be possible to send messages to the wrong mailbox (the one-to-one correspondence is about verifying adherence to Ravenscar rules in the face of suppressed SPARK checks on the mailbox array).