Great point! I have a "cheap" Samsung M32 that I bought for about $170. One reason I chose this Samsung phone over a similarly priced phone from a competitor was that I wrongly believed that Samsung provided several years more OS and security updates. After buying the phone I realized that longer support only applied to flagship models :/
It's not a toggle, but Google Pixel phones (or at least the one I owned a few years ago) come with very few if any bloatware type apps, since the default Android apps are the Google apps anyway. Contrast with Samsung that duplicates a bunch of core apps/functionality.
Are you aware of /The Implementation of Functional Programming Languages/ by Simon Peyton Jones, the main person behind the front end of the GHC Haskell Compiler? The full book is available free on his web site as PDF:
* the operations in the mathematical spec are mostly well defined, but e.g. division by zero is not defined. However, the verification handles this by checking that all operations are well-defined on all possible inputs.
* yes, identifying the "edge cases" is not something you can do easily, and hard to make formal. In some sense, the fact the non-edge-case inputs are treated in a uniform way is probably what allows the verification to succeed at all.
* a short summary of the answer you already found in the third blog post: what we actually verify is the LLVM assembly that Clang produces when compiling the C program. Much of the potentially undefined behavior in a C program is translated away by the compiler on the way to LLVM assembly. For any potential undefined behavior that remains in the LLVM assembly, the verification checks that it cannot happen at runtime.
I don't think I understand what you mean by "white-box testing" here, but perhaps it's helpful to clarify what I meant by "equivalence" above, and how it relates to testing: what we did here was verify input/output equivalence between the imperative C code and our functional mathematical spec in Cryptol, for a range of key and input buffer sizes. This corresponds to testing all inputs of those sizes, which is not possible to do by direct testing: e.g., for a 64 byte key and a 1000 byte message, the equivalence corresponds to checking
tests, which would take "forever" to verify by direct testing.
We did not prove any properties of our mathematical specification in Cryptol, but the claim is that it's close enough to the official FIPS mathematical specification for HMAC [1] that it's easy to believe that it's correct. However, a group at Princeton has also verified HMAC in the past, and gone further than us by not only proving that the imperative C code is input/output equivalent to their mathematical spec in Coq, but also proving that their mathematical spec has the security properties of a secure hash function [2].
Do you mean as opposed to e.g. verifying the absence of timing attacks? While I agree that verifying the absence timing attacks is probably much harder than what was done here, the difficult part of the s2n verification I linked to was that we verified equivalence between imperative C code and a functional mathematical specification.