Hi,
I like the Camkes (3) tool and believe it is essential for making seL4
accessible for developers. However, I have noticed some unexpected
limitations that I believe are either bugs or incomplete features.
Issue A:
A hierarchical component cannot have a dataport with a custom data type.
(However, a non-hierarchical component can have a dataport with a custom
data type. Also, a hierarchical component can have a dataport with a
built-in data type such as Buf.)
Issue B:
A dataport provided by a sub-component cannot be exported as a dataport
belonging to the hierarchical component that contains it. (However, the
export of event notifications from sub-components works just fine.)
Attached is the relevant code that demonstrates both issues, which is a
contrived example to highlight the issues without other stuff getting in
the way. Please note that the code as is compiles just fine, however if you
comment and uncomment a few lines of code (as instructed in Duck.camkes,
Duckherd.camkes and Duckling.camkes), the issues can be demonstrated
(separately) as compile failures.
There may be other issues with hierarchical components that I am not yet
aware of, as the above issues (unfortunately) have prevented me from
experimenting with them further.
Could you please acknowledge if these are issues that you are aware of, and
if there is likely to be a fix in a future Camkes 4 release?
Regards,
Dr Samuel Chenoweth
Cyber Security Researcher
DST Group
Note: I would have sent this email from my work email address (
samuel.chenoweth(a)dst.defence.gov.au) however I sent it from my personal
address instead because of issues to do with our email gateway. All the
contents of this email are UNCLASSIFIED and non-sensitive.
