Protection Profiles are descriptions of the security that must be provided by a system. They are used by government agencies to certify or evaluate conformance/suitability given certain security concerns. See the wikipedia articles:
In reading through the example, it seems to me that intent should perhaps facilitate a behavior where an application coder declares their intent to address a particular protection profile, and then the intent compiler tests that the code is hyperlinked or written in such a way that answers to each of the PP's questions is provable. For example, the referenced PP requires an application developer to declare a choice about "FCS_STO_EXT.1 Storage of Secrets". If the developer has told intent that this PP is a target, then the intent compiler should require that somewhere in the codebase, the developer has made an assertion about which storage-of-secrets strategy is in use. Perhaps it can go beyond that, by proving the non-use of functions/features that are marked to different storage-of-secrets semantics.
Protection Profiles are descriptions of the security that must be provided by a system. They are used by government agencies to certify or evaluate conformance/suitability given certain security concerns. See the wikipedia articles:
Here is an example protection file for a generic application: https://www.niap-ccevs.org/pp/pp_app_v1.1.htm
In reading through the example, it seems to me that intent should perhaps facilitate a behavior where an application coder declares their intent to address a particular protection profile, and then the intent compiler tests that the code is hyperlinked or written in such a way that answers to each of the PP's questions is provable. For example, the referenced PP requires an application developer to declare a choice about "FCS_STO_EXT.1 Storage of Secrets". If the developer has told intent that this PP is a target, then the intent compiler should require that somewhere in the codebase, the developer has made an assertion about which storage-of-secrets strategy is in use. Perhaps it can go beyond that, by proving the non-use of functions/features that are marked to different storage-of-secrets semantics.