Updating Carbon's safety strategy #5914
Conversation
chandlerc
added
proposal
chandlerc
force-pushed
the
safety-update
branch
from
44404fc to
69d8848
Compare
chandlerc
changed the title
github-actions
bot
added
proposal rfc
docs/design/safety/README.md
Outdated
| [evidence]: https://chandlerc.blog/posts/2024/11/story-time-bounds-checking/ | ||
| [performance control]: /docs/project/goals.md#performance-critical-software | ||
|
|
||
| The debug build will work to cause bugs and any detectable undefined behavior to |
There was a problem hiding this comment.
| The debug build will work to cause bugs and any detectable undefined behavior to | |
| The debug build will work to cause bugs in unsafe code and any detectable undefined behavior to |
There was a problem hiding this comment.
I want to include bugs in in safe code here. The safety guarantees may be by defining behavior even though it is erroneous, such as wrapping integer arithmetic. The debug build should try to make those bugs have fail-stop behavior.
There was a problem hiding this comment.
I think it would be nice to say that in the text then.
| efficient safety checks, it will remain important to improve the safety of code | ||
| for developers who cannot invest into safety-specific code modifications. | ||
|
|
||
| ## Principles |
There was a problem hiding this comment.
Perhaps we should keep this section (minus the hardened build mode)?
There was a problem hiding this comment.
A bunch of this content I thought was retained, although structured and phrased differently, and somewhat spread between proposal, strategy, and terminology.
I guess what would help me here is what particular parts of this are not adequately captured or implicit from Carbon's goals? And where could would they most effectively fit?
I'll also think a bit more about some of these and given them a more detailed read-through again to see what all I've missed.
|
|
||
| ## Caveats | ||
|
|
||
| ### Probabilistic techniques likely cannot stop attacks |
There was a problem hiding this comment.
This also seems like a valuable section to keep.
There was a problem hiding this comment.
Oh, yeah. This is definitely a good one to keep. I've created a "constraints" section of the design and moved it, but a) not sure that's the best name, maybe the "caveats" here is better? And b) I should go back through and link it to terminology and such.
Co-authored-by: Dana Jansens <[email protected]>
Co-authored-by: josh11b <[email protected]>
docs/design/safety/README.md
Outdated
| [evidence]: https://chandlerc.blog/posts/2024/11/story-time-bounds-checking/ | ||
| [performance control]: /docs/project/goals.md#performance-critical-software | ||
|
|
||
| The debug build will work to cause bugs and any detectable undefined behavior to |
There was a problem hiding this comment.
I want to include bugs in in safe code here. The safety guarantees may be by defining behavior even though it is erroneous, such as wrapping integer arithmetic. The debug build should try to make those bugs have fail-stop behavior.
docs/design/safety/README.md
Outdated
| The result is that Carbon does not have a "safe" mode and an "unsafe" mode, but | ||
| rather narrow and specific unsafe operations and constructs. | ||
|
|
||
| ## Safety modes |
There was a problem hiding this comment.
Yeah, a bit weird wording on my part.
I tried making the below modes more about strictness, but that didn't really work well either for me.
I came back and adjusted this to focus instead on the unsafe side of things and the fact that we don't consider whole regions or a "mode" of the language as completely unsafe. PTAL.
| efficient safety checks, it will remain important to improve the safety of code | ||
| for developers who cannot invest into safety-specific code modifications. | ||
|
|
||
| ## Principles |
There was a problem hiding this comment.
A bunch of this content I thought was retained, although structured and phrased differently, and somewhat spread between proposal, strategy, and terminology.
I guess what would help me here is what particular parts of this are not adequately captured or implicit from Carbon's goals? And where could would they most effectively fit?
I'll also think a bit more about some of these and given them a more detailed read-through again to see what all I've missed.
|
|
||
| ## Caveats | ||
|
|
||
| ### Probabilistic techniques likely cannot stop attacks |
There was a problem hiding this comment.
Oh, yeah. This is definitely a good one to keep. I've created a "constraints" section of the design and moved it, but a) not sure that's the best name, maybe the "caveats" here is better? And b) I should go back through and link it to terminology and such.
| - [Type safety]: compile-time enforcement, the same as other statically typed languages | ||
| with generic type systems. | ||
| - [Initialization safety]: hybrid of run-time and compile-time enforcement. | ||
| - [Spatial safety]: run-time enforcement. |
There was a problem hiding this comment.
This could be partially statically at compile time as well, no?
There was a problem hiding this comment.
I mean, the compiler may eliminate some of the runtime checks with compile time optimizations, but fundamentally the model is dynamic here just as it is in Rust. There is no systematic effort to propagate bounds as compile time parameters in the type system.
There was a problem hiding this comment.
How about a systematic effort to enable idiomatic Carbon code to be written in a way that makes those compiler optimizations possible?
There was a problem hiding this comment.
I'm not sure what systematic effort you're imagining here... There are things that are important here, but AFAIK, they are all things that all of C++, Rust, and Carbon will have in common like having range based for loops. I'm not sure there is much more than that to call out, and calling out basics like that seems like a distraction at this level?
There was a problem hiding this comment.
I think this may go beyond range based for loops. Like, functional idioms in general.
I think I was getting at to what extent idiomatic Carbon is going to "deprecate" index-based access. I don't think that this is "in common" with C++, because otherwise we wouldn't have spatial safety issues there.
There was a problem hiding this comment.
FWIW, I'm expecting us to largely succeed at deploying spatial safety in C++, without exceeding the runtime overhead thresholds described here.
I'm not expecting us to have a significantly larger focus on functional patterns than C++ (or Rust) in Carbon at this stage. Mostly, that is due to a lack of need (if spatial safety is achievable as-is in C++) and because every deviation from C++ is a cost.
| - [Type safety]: compile-time enforcement, the same as other statically typed languages | ||
| with generic type systems. | ||
| - [Initialization safety]: hybrid of run-time and compile-time enforcement. | ||
| - [Spatial safety]: run-time enforcement. |
There was a problem hiding this comment.
I'm not sure what systematic effort you're imagining here... There are things that are important here, but AFAIK, they are all things that all of C++, Rust, and Carbon will have in common like having range based for loops. I'm not sure there is much more than that to call out, and calling out basics like that seems like a distraction at this level?
| - [Type safety]: compile-time enforcement, the same as other statically typed languages | ||
| with generic type systems. | ||
| - [Initialization safety]: hybrid of run-time and compile-time enforcement. | ||
| - [Spatial safety]: run-time enforcement. |
There was a problem hiding this comment.
I think this may go beyond range based for loops. Like, functional idioms in general.
I think I was getting at to what extent idiomatic Carbon is going to "deprecate" index-based access. I don't think that this is "in common" with C++, because otherwise we wouldn't have spatial safety issues there.
docs/design/safety/README.md
Outdated
| annotation in audits and review. | ||
|
|
||
| The result is that we don't model large regions or sections of Carbon code as | ||
| "unsafe" or have a completely "unsafe" mode. We instead focus on the narrow and |
There was a problem hiding this comment.
I think maybe it'd be more clear to say "or have a completely unsafe parallel language" or "superset language" or something to that effect, instead of "mode" here?
There was a problem hiding this comment.
Hmm, maybe "parallel unsafe variant language"?
There was a problem hiding this comment.
I'm hesitant to make any claims about these modes that comes across like two-coloring the codebase. But maybe that's inherently going to happen? Not sure
There was a problem hiding this comment.
I'm mostly observing what I see with unsafe Rust today. Not sure if I would call it "two-coloring", but I do see there being basically two distinct variants in how you have to think about and work with code...
docs/design/safety/README.md
Outdated
| [evidence]: https://chandlerc.blog/posts/2024/11/story-time-bounds-checking/ | ||
| [performance control]: /docs/project/goals.md#performance-critical-software | ||
|
|
||
| The debug build will work to cause bugs and any detectable undefined behavior to |
There was a problem hiding this comment.
I think it would be nice to say that in the text then.
Co-authored-by: Dana Jansens <[email protected]>
Co-authored-by: Richard Smith <[email protected]>
docs/design/safety/README.md
Outdated
| annotation in audits and review. | ||
|
|
||
| The result is that we don't model large regions or sections of Carbon code as | ||
| "unsafe" or have a completely "unsafe" mode. We instead focus on the narrow and |
There was a problem hiding this comment.
I'm mostly observing what I see with unsafe Rust today. Not sure if I would call it "two-coloring", but I do see there being basically two distinct variants in how you have to think about and work with code...
Co-authored-by: Richard Smith <[email protected]>
| keyword: specific aspects of C++ interop or pervasive patterns that occur when | ||
| migrating from C++. However, not _all_ unsafe code will omit the keyword, the | ||
| permissive mode is designed to be minimal in the unsafe code allowed. | ||
|
|
||
| Modes can be configured on an individual file as part of the package | ||
| declaration, or an a function body as part of the function definition. More |
There was a problem hiding this comment.
or an a function body
"an" -> "on"? or "in"?
| While _cryptographic_ probabilistic techniques can, and typically do, work | ||
| carefully to not be subject to these weaknesses, they face a very different | ||
| challenge. The overhead of a cryptographically secure hash is generally | ||
| prohibitive for use in language level constructs. Further, some of the defenses |
There was a problem hiding this comment.
language level -> language-level
| carefully to not be subject to these weaknesses, they face a very different | ||
| challenge. The overhead of a cryptographically secure hash is generally | ||
| prohibitive for use in language level constructs. Further, some of the defenses | ||
| against hardware vulnerabilities and improvements further exacerbate these |
| @@ -25,6 +25,5 @@ wants to pursue, as well as those we want to exclude. | |||
| - [Information accumulation](information_accumulation.md) | |||
| - [Low context-sensitivity](low_context_sensitivity.md) | |||
| - [Prefer providing only one way to do a given thing](one_way.md) | |||
| - [Safety strategy](safety_strategy.md) | |||
| - A [hardened](#hardened) oriented build mode that prioritizes ensuring | ||
| sufficient safety to prevent security vulnerabilities, although it may not | ||
| allow detecting all of the bugs. |
There was a problem hiding this comment.
This document has old content.
Several minor fixes to the content in the `README.md` were pointed out in review after merging that are fixed here. I also accidentally undid the removal of the legacy strategy document. I _think_ I got all of the critical content from this incorporated into the safety design section, but if there is more that I missed, please flag and I'm happy to improve that as part of this PR as well.
|
Sorry for the delay, but got back to trying to address the comments here. Follow-up PR is #6013 |
Carbon is accelerating and adjusting its safety strategy, specifically to flesh out its memory safety strategy and reflect simplifying developments in the safety space.
This proposal replaces the previous directional safety strategy with a new concrete and updated framework for the safety design. It includes a specific framework for memory safety, simplified build modes, specific "safety modes", and terminology.
This proposal also provides a directional suggestion for temporal and data-race safety specifically.
In addition to fully building out the above directional component, there are several other aspects of our safety design that will follow in subsequent proposals. The hope is to establish the initial framework here.