Internal `fn encode_mut` seems to be unsound

[anforowicz]

I don't see how fn encode_mut (a safe function) guarantees the (implied) safety requirements of fn chunk_mut_unchecked:

data-encoding/lib/src/lib.rs

Lines 402 to 420 in a22931a

	fn encode_mut<B: Static<usize>, M: Static<bool>>(
	bit: B, msb: M, symbols: &[u8; 256], input: &[u8], output: &mut [u8],
	) {
	debug_assert_eq!(output.len(), encode_len(bit, input.len()));
	let enc = enc(bit.val());
	let dec = dec(bit.val());
	let n = input.len() / enc;
	let bs = match bit.val() {
	5 => 2,
	6 => 4,
	_ => 1,
	};
	vectorize(n, bs, |i| {
	let input = unsafe { chunk_unchecked(input, enc, i) };
	let output = unsafe { chunk_mut_unchecked(output, dec, i) };
	encode_block(bit, msb, symbols, input, output);
	});
	encode_block(bit, msb, symbols, &input[enc * n ..], &mut output[dec * n ..]);
	}

dec and i (on line 416) are produced by fn vectorize depending on n (derived from input on line 408) and bs (derived from bit on lines 409-413). There is no data dependency on output as far as I can tell. Therefore I don't see how fn encode_mut can guarantee dec * (i + 1) <= output.len() (the implied safety requirement of chunk_mut_unchecked). Therefore I think that fn encode_mut is unsound as currently written.

PS. This issue report is based on the audit from https://chromium-review.googlesource.com/c/chromium/src/+/6187726/comment/ae7a20dd_8c886e35/.

/cc @Manishearth
/cc @djmitche, @apasel422

[ia0]

Thanks for reaching out. I guess there are 2 possible responses depending on the problem:

1. encode_mut has a safety requirement described by its debug_assert. Whether this function is safe or not doesn't matter since it's a private function. I agree that it would simplify unsafe review to consider all functions "public" such that the presence of safety requirements is visible from the function being unsafe. But this style has a cost at each call site, so there's a balance. In this library, the presence of safety requirements is usually visible from the presence of debug assertions (but not always, in particular for type invariants). That said, if you argue that considering all functions "public" would considerably help unsafe review, I would consider following that style.

2. The safety requirement that output.len() == encode_len(bit, input.len()) gives you the missing link. Here are the steps:

   • (i + 1) * enc <= input.len() was discharged with chunk_unchecked (I assume you agree with this since you only mention chunk_mut_unchecked)
   • (i + 1) * enc * 8 / bit <= input.len() * 8 / bit by multiplying both sides by 8 / bit (mathematically, no integer division)
   • (i + 1) * dec <= input.len() * 8 / bit by the definition of dec
   • output.len() = encode_len(bit, input.len()) by function precondition (the safety requirement)
   • output.len() = trunc((8 * input.len() + bit - 1) / bit) by the definition of encode_len
   • (8 * input.len() + bit - 1) / bit - 1 < output.len() by the lower bound of trunc¹
   • 8 * input.len() + bit - 1 - bit < output.len() * bit by multiplying both sides by bit
   • 8 * input.len() <= output.len() * bit by simplification
   • input.len() * 8 / bit <= output.len() by dividing both sides by bit (mathematically)
   • (i + 1) * dec <= output.len() by transitivity

Footnotes

1. x - 1 < trunc(x) <= x ↩

[Manishearth]

But this style has a cost at each call site, so there's a balance. In this library, the presence of safety requirements is usually visible from the presence of debug assertions (but not always, in particular for type invariants). That said, if you argue that considering all functions "public" would considerably help unsafe review, I would consider following that style.

I do think this style is preferred, aside from unsafe things that are very narrowly scoped to a smal lsection of a file.

As someone reviewing unsafe code it makes it possible to quickly check if things are correctly safety-commented. As someone writing near unsafe code it gives me peace of mind that my changes to the codebase won't break anything. And as someone reviewing unsafe code, knowing that the maintainers have that additional backstop against mistakes is a big plus, too.

My broad rule of thumb for good unsafe code is that it should be dead simple to review, just a matter of following the breadcrumbs left by comments. Each safety block has a comment saying what invariants need to be upheld for it, and how they are upheld, so verifying unsafety becomes a matter of verifying that the list of invariants are exhaustive, and that the comments explaining how the invariants are upheld are true. You don't need to hold a lot of cross-crate state to chase down invariants.

I don't hold this position because I think "easy to unsafe review" is easier on unsafe reviewers, I hold it because it's a good bar for good safety comments, which, again, benefit the maintainers.

[anforowicz]

Thank you very much for your comments. I appreciate the feedback. And the explanation of how the safety reasoning works in fn encode_mut is quite helpful.

---

Whether this function is safe or not doesn't matter since it's a private function. I agree that it would simplify unsafe review to consider all functions "public" such that the presence of safety requirements is visible from the function being unsafe.

I note that the same argument could be applied to unsafe fn chunk_unchecked which nevertheless is marked as unsafe.

---

One reason why I am mainly circling back is to admit that there is indeed some subjectivity and flexibility in how things are designed. OTOH, I wanted to point external resources that made me lean toward treating fn encode_mut as unsound:

• Rust reference: https://doc.rust-lang.org/reference/unsafe-keyword.html#unsafe-blocks-unsafe-
  • By putting operations into an unsafe block, the programmer states that they have taken care of satisfying the extra safety conditions of all operations inside that block.
  • Unsafe blocks are the logical dual to unsafe functions: where unsafe functions define a proof obligation that callers must uphold, unsafe blocks state that all relevant proof obligations of functions or operations called inside the block have been discharged. There are many ways to discharge proof obligations; for example, there could be run-time checks or data structure invariants that guarantee that certain properties are definitely true, or the unsafe block could be inside an unsafe fn, in which case the block can use the proof obligations of that function to discharge the proof obligations arising inside the block.
• Auditing standards described in https://github.com/google/rust-crate-audits/blob/main/auditing_standards.md
• Clippy lints like:
  • https://rust-lang.github.io/rust-clippy/stable/index.html#undocumented_unsafe_blocks
  • https://rust-lang.github.io/rust-clippy/stable/index.html#missing_safety_doc (I recognize that by default check-private-items is false for this lint; I personally don't like this default...)

---

One more question: would it be possible to avoid some of the safety concern by deleting fn chunk_unchecked and fn_chunk_mut_unchecked and tweaking their callers to instead use chunks_exact and chunks_exact_mut from the Rust standard library?

(I assume that the library here assumes "exact" chunking. If not, then there are also chunks and chunks_mut.)

[ia0]

I don't hold this position because I think "easy to unsafe review" is easier on unsafe reviewers, I hold it because it's a good bar for good safety comments, which, again, benefit the maintainers.

I agree. So far I'm the only maintainer and plan to be until my death, so it doesn't matter for this purpose. But it holds for maintainers after my death. By then (I'm not planning to die in the next 10 years), there will be a formal proof of correctness (and thus soundness), which will anyway enforce this style, and thus help the future maintainers get started. So I agree, why not start now.

I note that the same argument could be applied to unsafe fn chunk_unchecked which nevertheless is marked as unsafe.

That's because I'm hoping to eventually use a drop-in replacement from the standard library. So I want a look-and-feel as close as possible.

I wanted to point external resources

• Rust reference

Those only say what unsafe blocks and unsafe functions mean, not what safe blocks and safe functions mean. In particular, they wouldn't be able to, because the language just doesn't give the expressivity to track safety with unsafe at any scope. That's why there's this notion of scope of unsafe. For example, Vec::set_len() should really use an unsafe block, but doesn't until we have unsafe fields.

Also later the reference says: "Unsafe blocks are used to wrap foreign libraries, make direct use of hardware or implement features not directly present in the language". So they really mean that it only matters at abstraction barriers.

(Note that I'm arguing on this from a technical perspective only. I agree with you that the formal style is preferred.)

• Auditing standards

Those are quite new. The current code of this library was written 7 years ago. At that point, there was no concept of unsafe review on the horizon. I didn't expect anyone to review my code. I expected them to review my fuzzing targets.

• https://rust-lang.github.io/rust-clippy/stable/index.html#undocumented_unsafe_blocks

This library wasn't written for unsafe review. I agree this is a nice lint and I should probably enable it.

• https://rust-lang.github.io/rust-clippy/stable/index.html#missing_safety_doc (I recognize that by default check-private-items is false for this lint; I personally don't like this default...)

That's the style question. I agree with the style ultimately, but within the scope of unsafe, you're theoretically free to do what you want.

One more question: would it be possible to avoid some of the safety concern by deleting fn chunk_unchecked and fn_chunk_mut_unchecked and tweaking their callers to instead use chunks_exact and chunks_exact_mut from the Rust standard library?

That's a good point. I don't remember if I tried and wasn't satisfied with the performance (losing the manual vectorization). But I'm starting more and more to consider losing on performance for other benefits (like review).

Action items for me before closing this bug (no ETA, but I hope I'll get time this weekend):

• Convert the code to the formal style of unsafe.
• Enable the recommended lints: https://ia0.github.io/unsafe-mental-model/unsafe-reviews.html#recommended-lints
• Consider again using chunks_exact{_mut}.

[ia0]

I took a look at the 3 action items in #125:

• I have mixed opinions on the formal style, see below.
• Enabling the lints was not an issue.
• Using chunks_exact{,_mut} has a 15% performance regression, but it seems due to the missed vectorization only. So if I decide to remove the vectorization, then I could use chunks_exact{,_mut}.

I care about correctness (soundness is just a side-effect). So it makes no sense for me to annotate pre- and post-conditions for safety only. The separation between correctness and soundness can move as needed for optimization purposes. So I'm annotating for correctness, and if a requires or ensures is relevant for soundness, I suffix it with (safety). A function is unsafe if and only if it has at least one requires(safety).

Another problem is that Rust doesn't have a notion of robust, just unsafe. This means that functions with at least one ensures(safety) don't have any syntactic tell that there must be a SAFETY comment that the guarantee holds (it should be a robust fn). This problem is described in more details in the unsafe mental model.

Given this is just for unsafe reviewers and future maintainers, this doesn't feel that useful. For unsafe reviewers, the crate has been stable for 8 years, modifications never touch unsafe code in non-trivial way, so the cost is only on the initial review. Diff reviews should be trivial. For future maintainers, I expect all those annotations to be formal in v3. In particular, they would be automatically checked and thus maintained. This would also be useful for unsafe review of v3, since only the propositions need to be reviewed to make sure they cover the safety requirements. The proofs don't need to be reviewed and won't be written unless the tool needs hints.

I'm gonna sleep on this some more to see if I find a better solution for v2. If no, then I'll just finish annotating the remaining functions.

[ia0]

Sleeping on it, I realize that trying to distinguish between correctness and soundness on internal functions is extremely painful and error-prone. Here are some examples:

• enc and dec don't really need to ensure their correctness postcondition for soundness, we just need the following weaker lemma that 8 * enc(bit) == bit * dec(bit) for all 1 <= bit <= 6 (no need to divide by gcd(8, bit), any common denominator would do).
• Functions taking symbols: &[u8; 256] don't really need the symbols to be ASCII if they guarantee that they write to the output from symbols (or from the correct symbol as guaranteed for correctness). If they require symbols to be ASCII, then they only need to guarantee that the output is ASCII for soundness (still guaranteeing that the output comes from the correct symbol for correctness).
• Depending on the choice above, you either need to make chunks_mut_unchecked guarantee that it returns the appropriate sub-slice for soundness or not. Actually, this also depends on whether the functions taking symbols also require the output to be ASCII already (which you don't need for correctness).

So I see at least 4 options:

• All functions are annotated for correctness, and all annotations are used for soundness. This means some functions will be made unsafe even though they would be also sound if safe. That's usually frown upon in Rust, because unsafe is not meant to be used for correctness on public functions. That's also bad for readability by having too many unsafe blocks.
• All functions are annotated for correctness, and a subset of the annotations is used for soundness (not trying to be minimal on the subset, because it's possible different incomparable minimal subsets would work). This has a maintenance cost for the purpose of unsafe reviews only (namely having internal unsafe functions, not something that Rust recommends).
• All functions are annotated for correctness, and no annotations for soundness. That's definitely the best option for maintenance. But it makes unsafe reviews harder because one can't easily distinguish correctness from soundness, and essentially has to do a correctness review instead of just a soundness review.
• No annotations. That's the best for maintenance as long as I'm alive. That's definitely not the best for unsafe reviews.

#125 is currently taking the second approach. The current code is the fourth approach. I would tend for the third approach, because the second approach adds rather unjustified maintenance cost for the purpose of unsafe reviews only.

Would the third approach work for unsafe reviews?

[ia0]

I do think this style is preferred

AFAICT, this style doesn't exist in Rust today. The only place I've seen it, is in the unsafe mental model. Please provide a link if you know another place where this style is documented. The current style in Rust is:

• For public functions: document correctness and safety. The safety documentation defines the conditions for library UB. In particular, it is not a contract to prove program soundness in a modular way, since it doesn't guarantee anything more than the function soundness. This is in contrast with the correctness documentation (resp. the soundness documentation of the unsafe mental model), which is the contract to prove program correctness (resp. program soundness) in a modular way. In particular, today, to prove program soundness in a modular way (as unsafe reviews seem to be attempting), you need to use correctness contracts (usually for the language, private functions in the scope of unsafe, the standard library, and possibly hand-picked crates) in addition to safety contracts (from both language and libraries, which define undefined behaviors and thus soundness). See this zulip thread for details.
• For private functions: there is no style. In particular, the implementation is the specification for all purposes (correctness, soundness, safety, etc).

So I'm solving this issue with the following steps and observations:

• I've added safety annotations and assertions in Add missing safety documentation and assertions for testing and fuzzing #128 (the assertions are checked during testing, fuzzing, and any other build with debug assertions). In particular, I'm only using unsafe blocks since the public API is safe and the private functions are specified by their implementation (see last point). There's no need for private unsafe functions.
• The step above works by observing that all unsafe operations in this library can easily be checked without Miri. Miri is still being used for testing since 2 years Run tests with Miri #59, even though it doesn't add any benefit at this time (but it will in v3).
• Fuzzing is exhaustive over encodings and inputs (there is a fuzzing input for any pair of encoding and input) since 4 years. So it is akin an automatic soundness proof at the limit.
• Besides fuzzing properties of the specification, I'm also now fuzzing for correctness since Improve fuzzing #129. So fuzzing is also an automatic proof of correctness at the limit. This is not directly useful for soundness, but for this purpose, a reference implementation was added in lib/fuzz/src/spec.rs which can be used to follow the optimized implementation in lib/src/lib.rs for manual review purposes (and in particular to have a more formal specification in Rust in addition to the informal one in English prose).