[RFC] Sensitive aspect

[Blady-Com]

RFC proposal for Sensitive aspect for Ada and SPARK languages.

link to proposal: https://github.com/Blady-Com/ada-spark-rfcs/blob/sensitive/considered/rfc-sensitive.rst

[Glacia]

1) This feature needs a better name, "Sensitive" tells me nothing, i would be very confused to see this in code. 2) Why this should be an aspect? Shouldn't this be achievable with controlled types? Seems like a lot of work for a feature 99% of people wouldn't use. 3) Is there really any use case for "cleaning value" to be non zero?

Overall, this feature seems very raw, but i support the idea of getting more security related functionality in Ada.

[QuentinOchem]

Interesting one. There's definitely interest in allowing sensitive data to be sanitized, this is not the first time the requirement comes up. There's probably several different ways to do it and it's unclear which would be the best approach, but a few comments to push this proposal a notch further:

• I would make the comment:

  Add a compiler warning if all or a part of a sensitive object is transfered to a non sensitive object.

an integral part of the proposal. This seems quite fundamental to make sure the sensitive values aren't "escaped".

• I would have some extra details in the case of dynamic memory. How do you mark dynamic memory to be sensitive? Is it a property of the access type? the access variable? The accessed object or type?

[Blady-Com]

1. This feature needs a better name, "Sensitive" tells me nothing, i would be very confused to see this in code.

As I'm not a native English speaking, I'm not in a confortable position concerning the idiomatic name meaning. Well Sensitive is defined, among others, in Collins as "reflecting national security" and in as Oxford "kept secret or with restrictions on disclosure to avoid endangering security: he was suspected of passing sensitive information to other countries.". This meaning says more than possible others as Sanitizing or Cleaning. It aimed to say more semantic meanings that only "the variable should be sanitized": the hold value is itself concerned. Many others actions would be taken concerning propagating the sensitive value and warn the user if not secure.

2. Why this should be an aspect? Shouldn't this be achievable with controlled types? Seems like a lot of work for a feature 99% of people wouldn't use.

Using controlled types is a partial possible workaround with current Ada. Quid of the required cleaning value (project or even customer dependant) which should be valid for the type? One may add Unchecked_Union with a cleaning field of the adequate size with custom needed Finalize operation. But why programers would have care about all of that when the compiler would do it better?

3. Is there really any use case for "cleaning value" to be non zero?

Yes, the required value may be project defined or even a customer requirement.

Overall, this feature seems very raw, but i support the idea of getting more security related functionality in Ada.

Thanks for supporting the idea, it would be a drastic plus for Ada to include some "secure ready" functionalities.

[Blady-Com]

Interesting one. There's definitely interest in allowing sensitive data to be sanitized, this is not the first time the requirement comes up. There's probably several different ways to do it and it's unclear which would be the best approach, but a few comments to push this proposal a notch further:

• I would make the comment:

Add a compiler warning if all or a part of a sensitive object is transfered to a non sensitive object.

an integral part of the proposal. This seems quite fundamental to make sure the sensitive values aren't "escaped".

Yes I agree, but it should not prevent an implementation of Sensitive aspect which don't support warning. Maybe an implementation might build this functionality step by step as it wouldn't be trivial.

• I would have some extra details in the case of dynamic memory. How do you mark dynamic memory to be sensitive? Is it a property of the access type? the access variable? The accessed object or type?

The memory becomes sensitive when allocating memory with new rather than accessing a variable. Let introduce an example:

   type Key_Access is access all Integer with Sensitive;
   K : aliased Integer;
   KA1 : Key_Access := new Integer;
   KA2 : Key_Access := K'Access;

KA1 is accessing dynamic memory that will be sanitized when calling Free; (Note in the above example no value is given for memory location KA1 which will be though sanitized) KA2 is accessing variable K, in this later case the responsibility for sanitizing is on K (here no Sensitive aspect on K thus nothing will be done). Well we should advice that "access all" with Sensitive aspect is a bad practice. Any further comments is welcome.

[QuentinOchem]

The memory becomes sensitive when allocating memory with new rather than accessing a variable. Let introduce an example:

   type Key_Access is access all Integer with Sensitive;
   K : aliased Integer;
   KA1 : Key_Access := new Integer;
   KA2 : Key_Access := K'Access;

KA1 is accessing dynamic memory that will be sanitized when calling Free; (Note in the above example no value is given for memory location KA1 which will be though sanitized) KA2 is accessing variable K, in this later case the responsibility for sanitizing is on K (here no Sensitive aspect on K thus nothing will be done). Well we should advice that "access all" with Sensitive aspect is a bad practice. Any further comments is welcome.

Thanks for these extra details. You seems to indicate that "Sensitive" is then a property of the access type. It may seem a bit inconsistent then to allow to point both to sensitive data (KA1) and non-sensitive ones (KA2). While I think it's a good idea to indeed apply the property on the access type, I think this calls for further work in the previous point of preventing data leaking from sensitive to intensive places. KA2 is weird here because it's assigned pointing to non-sensitive data, even if the type is sensitive. And what to say of parameters or any place where it's not easy or even possible to tell what they're pointing to.

In light of your example, I would argue that rules of mixing sensitive and non-sensitive data should be clarified by the RFC, and that violations should be an error, not a warning, possibly worked-around though "Unchecked" notations. Not unlike what Ada is already doing through e.g. accessibility checks.

[raph-amiard]

I agree with @Glacia about the name of the feature, and also about the fact that a language level extension feels heavy for this (even though it's on the lightweight side, being only an aspect).

However @Glacia:

Shouldn't this be achievable with controlled types ?

OP explains why this is not desirable: SPARK doesn't have controlled types, and might not ever.

Is there really any use case for "cleaning value" to be non zero

This is explained in the OP's presentation that is linked in the RFC https://www.auto.tuwien.ac.at/~blieb/AE2017/presentations/ae2017_chapman.pdf.

@Blady-Com, I like the idea very much, however I'll remain firmly in the camp of "library level improvements", and think we should explore every opportunity to make this feature available as a library level feature if at all possible.

Thinking in terms of structural/generic typing, this is really something like a Sensitive<T> type, with strict but user definable rules about how to go from a Sensitive<T> to a T. Discussing this with @yannickmoy, there might be a possibility to express this via generics and controlled types, hiding the controlled part away from SPARK.

Unavailability of controlled types in certain runtimes might be a problem, but then anyway to implement this feature you need to implement something "akin to" controlled types.

EDIT: Note that, since in the context of other RFCs, we're discussing improvements to generics (for example), I'm not saying we should absolutely build this with existing language features, but more that we should think about whether this could be expressed fluently with a few missing bits and pieces.

[Blady-Com]

In light of your example, I would argue that rules of mixing sensitive and non-sensitive data should be clarified by the RFC, and that violations should be an error, not a warning, possibly worked-around though "Unchecked" notations. Not unlike what Ada is already doing through e.g. accessibility checks.

Well, the proposal doesn't aim to enforce some stricts rules (and maybe complicated) about mixing sensitive and not sensitive data. The aim is rather to be sure that an object marked with Sensitive aspect by the programmer won't let sensitive value in the memory when the object no longer needed by the program. Thus a warning seems to me correct or even a compiler option will consider the warning as an error (as it is the case for GNAT). Obviously, the following (even if no data are transferred) would issue a warning:

   KA2 : Key_Access := K'Access;

Mixing mixing sensitive and not sensitive data issue would rather be integrated in a larger issue of mixing different integrity level data domains. I hope I might be able to propose a future Ada RFC on that topic.

[Blady-Com]

@Blady-Com, I like the idea very much, however I'll remain firmly in the camp of "library level improvements", and think we should explore every opportunity to make this feature available as a library level feature if at all possible. ... Unavailability of controlled types in certain runtimes might be a problem, but then anyway to implement this feature you need to implement something "akin to" controlled types. EDIT: Note that, since in the context of other RFCs, we're discussing improvements to generics (for example), I'm not saying we should absolutely build this with existing language features, but more that we should think about whether this could be expressed fluently with a few missing bits and pieces.

Improvement of generics and controlled types are certainly a good thing and might be used as underlying technology bricks to implement the Sensitive aspect in the compiler. In other words, the compiler might implement "My_Key : Key_Type := Get_Key with Sensitive;" as if My_Key was a tagged controlled objet with some inner Finalize procedure doing the job. I'm convinced that beyond sanitizing memory actions, the compiler would take other actions to avoid that sensitive values will be spread in cache memory or even disk virtual memory (some operating system encrypt their cache or disk memory). It seems to me that the compiler should be aware of sensitivity of the objets whatever the manner.

[yannickmoy]

I'd like to separate out requirements, to isolate the core of this RFC from what should be pursued in others:

1) The need to cleanup sensitive data by calling a destructor at the end of the life of the sensitive object. This is the core of this RFC. It could be implemented today as a generic library building on top of controlled objects. In particular, it would be possible to implement the various options proposed by @Blady-Com to zero-out the whole object or fill it with a predefined pattern, by taking internally the address of the aliased component, converting it to an array of bytes and doing the cleanup.

2) The need to avoid sensitive data from leaking. This should be done with SPARK flow analysis IMO.

3) The need to avoid sensitive data from being scattered over multiple layers of memory: disk, RAM, caches, registers. It's beyond the topic for this RFC. An interesting venue to explore is the capability to ensure such a property for a memory-pool, for a certain combination of processor and Operating System (or bare-metal i.e. no OS).

Questions that should be answered on this RFC regarding (1) are:

• Is a library solution as proposed usable in the current state?
• If not, what are the problems? Integration in SPARK code which forbids controlled types? Compilation for a given runtime that does not support controlled types? Something else?

Questions related to (2) and (3) should be dealt with in other RFC I think, to allow focusing this one on the cleanup part.

[sttaft]

Finalization is much easier in the absence of exception propagation, since there is generally less need of "keeping track" of where you are in the process of initializing a set of objects of the same scope, since we presume that once you start initializing the objects of a given scope you will finish doing so. The only places where finalization needs to be worried about are on explicit transfers of control out of a scope, plus on the normal completion of a scope. All of these places are well known to the compiler, and a call on the relevant finalization code can be placed "statically" by the compiler (and probably already is by GNAT). So supporting controlled types in the absence of supporting exception propagation is something that would seem pretty manageable in SPARK.

On Thu, Jul 25, 2019 at 5:30 AM yannickmoy notifications@github.com wrote:

I'd like to separate out requirements, to isolate the core of this RFC from what should be pursued in others:

1.

The need to cleanup sensitive data by calling a destructor at the end of the life of the sensitive object. This is the core of this RFC. It could be implemented today as a generic library building on top of controlled objects. In particular, it would be possible to implement the various options proposed by @Blady-Com https://github.com/Blady-Com to zero-out the whole object or fill it with a predefined pattern, by taking internally the address of the aliased component, converting it to an array of bytes and doing the cleanup.

...

-Tuck

[raph-amiard]

@yannickmoy @Blady-Com I'm giving you the job of extracting what you think should be kept from this, and eventually closing this RFC and opening new ones, since it's clear that while the ideas are interesting, they're not in a form that is mature enough to consider even prototyping at this stage.

There seems to be a part of that that has been covered by the finalization working group.

@Blady-Com do you have any time to discuss with @yannickmoy on top of the previous comment he made, to see whether something can be extracted ?

Thanks guys in advance

[yannickmoy]

@Blady-Com A Machine_Attribute named strub has now been implemented in GCC, to trigger stack scrubbing when a subprogram reads a given variable. There are other options to annotate directly a subprogram, or even types. See the GNAT Reference Manual.

That seems to address your need, what do you think?

[Blady-Com]

Le 21 avr. 2022 à 09:05, yannickmoy @.***> a écrit :

@Blady-Com A Machine_Attribute named strub has now been implemented in GCC, to trigger stack scrubbing when a subprogram reads a given variable. There are other options to annotate directly a subprogram, or even types. See the GNAT Reference Manual.

That seems to address your need, what do you think?

I've read all "Security Hardening Features" section. I'm happy to discover security topics in GNAT :-)

Concerning stack scrubbing, it looks promising at first sight.

Some good points, I'm seeing:

• it applies on subprograms and their callers
• it applies on variables (I guess on constants too?)
• it applies on types (It seems to me yes?)

Some questions:

• I can't figure out what is for the purpose of "strub" with "internal"? Comments aren't so understandable for me.
• Does "strub" apply to main program? In order to scrub its stack when program is ending.
• When using this pragma could be happen side effects with SPARK?
• Is it also available in C or C++?
• In the access code example, shouldn't VI and VSI be aliased?
• In the access code example, shouldn't "strub" pragma be added to VI?
• In the access code example, shouldn't the XsVSI comment similar to the Var comment in the previous example? "Reading from XsVSI.all in a subprogram..."
• Does the compiler scrubbing code will be certified? In order to give assurance of its proper functioning for national assessors for instance.
• About Ada secondary stacks, is there a mean in GNAT to know when they are activated? On which items?
• Shouldn't be needed to specify a specific scrubbing value instead zero?

Thanks Yannick for your support, Pascal.

[yannickmoy]

Happy to see that you like it Pascal! In a nutshell: yes, all of these apply to Ada and C, some to C++. And we did some fixes to the doc that are not yet visible. For details, they will be in the FSF GCC manual ("Using the GNU Compiler Collection (GCC)") once the respective features are accepted upstream. Currently, you can read them in the version of GCC manual that we ship with our products.

[yannickmoy]

Closing this PR now, as this is taken care of with machine attributes in GCC, for Ada and other languages.