10 ms·

So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-S

So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)? I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.

kaba0 5y ago
Formal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.
- hulitu 5y ago
  Testing is hard. And (very) expensive.
  - kaba0 5y ago
    Formal verification is even harder. And even more (very) expensive.
- tonyarkles 5y ago
  In a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons: - the requirements generally change quite frequently - the requirements are generally a long way from being "formally verifiable" Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work: - A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states. - A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases. - Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
  - kaba0 5y ago
    Thanks for the informative answer! Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.
    - Y_Y 5y ago
      > TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.
      - kaba0 5y ago
        But it only proves a model, not the actual code — that’s a major distinction.
    - hwayne 5y ago
      It's formal verification of an abstract machine as opposed to running code. The problem is that formal methods as a field doesn't yet have a rich enough vocabulary to distinguish between its flavors. I use "code verification" and "design verification", which is a little more specific, but has its own issues. Is TLA+ a sandwich?
  - mmis1000 5y ago
    You can't write a bug and nor can you write a test if you don't even have proper spec. But it happens a lot when requirements are just ambiguous.
- grumblenum 5y ago
  I was under the impression that SeL4 exists.
  - raphlinus 5y ago
    Kinda. https://news.ycombinator.com/item?id=27232401 https://news.ycombinator.com/item?id=27232401 I think CSIRO disbanding the team was a huge mistake, but in any case they weren't producing the kind of success metrics that sustained their funding.
    - dnautics 5y ago
      I know of at least one other company that is picking it up.
  - MaxBarraclough 5y ago
    That's true, but as a microkernel, seL4 has a very limited scope. It's not in the same ballpark as, say, the Linux kernel. It's more like a hypervisor. [0] From a quick google, seL4 has around 10,000 lines of C code, whereas the Linux kernel has around 30,000,000. [0] https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf
- johnisgood 5y ago
  https://github.com/Componolit https://github.com/Componolit Let us see what they have, using formal verification (Ada/SPARK). - JWX is a library for handling JSON data and more. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. As a result, JWX is particularly suited for processing untrusted information. - The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by Ada. A detailed description of the language elements can be found in the Language Reference. - Formally verified, bounded-stack XML library This is just Componolit. Let us check the F* language: - F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives. --- Given the above, what exactly do you mean that it does not scale?
  - johnisgood 5y ago
    Whoops, I completely forgot about libsparkcrypto (https://github.com/Componolit/libsparkcrypto https://github.com/Componolit/libsparkcrypto) which is a "formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.". Features: * AES-128, AES-192, AES-256 * AES-CBC (all supported AES modes) * SHA-1 * HMAC-SHA1 * SHA-256, SHA-384, SHA-512 * HMAC-SHA-256, HMAC-SHA-384, HMAC-SHA-512 * PRF-HMAC-SHA-256, PRF-HMAC-SHA-384, PRF-HMAC-SHA-512 * RIPEMD-160 * HMAC-RIPEMD-160 * ECDSA, ECGDSA It is pretty awesome. :)
    - dexterlemmer 5y ago
      Looking at the examples you've provided, I'm pretty sure the Linux kernel's codebase dwarfs their combined codebases into insignificance. Since it is very hard to not have NP-hard asymptotic complexity when formally verifying a codebase as large and as demanding (in terms of performance, etc) as the Linux kernel, I would expect that if you tried to rewrite Linux in the languages you've mentioned and formally verify the rewrite, you will be able to keep the entire AWS cloud (globally) very busy for a very, very long time. On the other hand, if you were to do the rewrite in Rust and use some hypothetical formally verified Rust compiler to type check it (which is mathematically equivalent to such a formal verification in, say, F* limited to only verifying certain properties), it'll probably type check in minutes or even seconds on the laptop I'm currently writing this reply on. For a less hypothetical example. RedoxOS has a codebase that dwarfs Sel4 (but it is still much smaller than Linux in turn), yet it type checks with much less compute cost than it takes to formally verify Sel4. Or heck, Redleaf actually formally verifies in a tiny fraction of the time it takes to formally verify Sel4, because the Rust type checker not only significantly reduces the amount of requirements that still needs to be formally verified but also reduces the complexity to verify those requirements to linear to the codebase size due to the restrictions that the Rust type system and module system puts on valid Rust programs (with a little bit of care when writing the code). Of course, until you have a certified Rust compiler there might still be miscompiles of Redleaf and until all the features of Rust used in the Linux kernel is formally specified, we cannot do the same with the Linux kernel as for Redleaf even if somehow all of Linux got rewritten in Rust. But in Rust at least it is conceivably possible given sufficient resources and sufficient time. I very much doubt it will ever be possible without help from a sufficiently expressive and practical type system. Oh yea. Then there's another problem. Most (all?) of the examples you've mentioned have requirements that are well specified and pretty much set in stone. The requirements fro the Linux kernel... aren't quite as obliging.
- dnautics 5y ago
  Sel4 is an OS that is formally verified. It's security parameters are well-defined enough that you can use it to launch isolated VMs with... less secure OSes that are sandboxed from each other.
lmm 5y ago
Rust has far more enthusiasm from potential contributors than any of those options. Onboarding something is meaningless if it's not going to be used and maintained. FWIW I would trust anything language-level over applying static analysis tools to C (for an evolving codebase like Linux, having the safety be a first-class part of the codebase is a must) or extracting C from another language (the semantics of C are surprisingly weak, such an extraction can only ever be as good as your model of C which will probably be buggy).
zozbot234 5y ago
> I've never read anything to make me think that Rust is a safer alternative than any of these options What Rust focuses on is providing a scalable approach to a limited kind of formal verification - focusing purely on type- and memory-safety, not conformance to arbitrary specifications. The latter is of course being worked on, but type safety and memory safety are table stakes.
- grumblenum 5y ago
  > focusing purely on type- and memory-safety, not conformance to arbitrary specifications What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?
  - zozbot234 5y ago
    Types are not 'arbitrary' in any real sense. Type systems can be described as a sort of formal verification that leverages and is closely aligned with the syntax structure of actual code, thus type systems can preserve compositionality but don't generally support non-local reasoning, at least not in a very elegant way. This is exactly what can make them potentially more scalable than other sorts of FV, hence more useful for programming "in the large".
    - grumblenum 5y ago
      Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.
      - PhaseLockk 5y ago
        Maybe I can try to explain the parent comment's point a different way. When saying that rust works on types and not on arbitrary specifications, I think he is saying that rust is more limited than languages that support arbitrary specifications. However, by making this tradeoff it achieves a reasonable degree of safety without incurring a ton of overhead. I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec. When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system. Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.
erk__ 5y ago
Its not like Microsoft does not work on that, they probably have a dozen different formally verified programming languages around at the moment. You already mentioned F*[0], but there is also Checked C[1], VCC[2], koka[3], dafny[4], Project Verona and probably some more that I am missing. The point being that they have clearly evaluated and have used F-Star for parts of the OS already. [0]: https://www.fstar-lang.org https://www.fstar-lang.org [1]: https://www.microsoft.com/en-us/research/project/checked-c/ https://www.microsoft.com/en-us/research/project/checked-c/ [2]: https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ https://www.microsoft.com/en-us/research/project/vcc-a-verif... [3]: https://github.com/koka-lang/koka https://github.com/koka-lang/koka [4]: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5]: https://www.microsoft.com/en-us/research/project/project-verona/ https://www.microsoft.com/en-us/research/project/project-ver...
ngrilly 5y ago
Static code analysis is not enough for C: https://t.co/Pbo4iHqEub https://t.co/Pbo4iHqEub
- jsymolon 5y ago
  no twitter https://sheas.blog/papers/The_Challenge_of_Using_C_in_Safety_Critical_Applications.pdf https://sheas.blog/papers/The_Challenge_of_Using_C_in_Safety...
  - ngrilly 5y ago
    Apologies. I thought I pasted the original link but I was wrong. Thanks for fixing it.
deleted 5y ago
[deleted]
geofft 5y ago
As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it. I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work. Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust. I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem. If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!
- pjmlp 5y ago
  > What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. It does, just not the way most are used to it. Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {} However many type constructions in Ada do dynamic allocation by themselves, including on the stack. If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.
  - tialaramex 5y ago
    > If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis. Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.
nonameiguess 5y ago
Without being an expert in either language, given what Ada is used for, I'm sure it offers at least all of the safety Rust offers and probably more. But Rust has a lot more going for it than safety. Maybe it shouldn't matter for kernel code, but the focus on developer "ergonomics," high-level functional constructs and pretty flexible pattern matching, supporting both ML-style and Algol-style syntax, very strong language-level tooling for building, testing, packaging, and generating documentation, plus the fact that the language itself is so well documented with great, accessible tutorials. There's a reason it keeps winning Stack Overflow's most loved language award every year. It's easy to learn for people coming from almost any kind of programming background, supportive of newbs, and equally well-suited for application-level and system-level development, so it ends up with pretty widespread appeal. So again, I don't know that any of this should matter for selecting what languages you're going to support in the kernel, but as a purely practical matter, it's a lot easier to ask contributors to use a language they already know and use elsewhere than it is to ask them to learn something new that they don't use anywhere else, which is what Ada and Idris and what not would be for most developers.
rkangel 5y ago
> I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates. Note that some formal verification work has been done on the guarantees that the borrow checked provides (which led to finding and fixing an edge case bug), so there is a little more concrete evidence that just the "assurances of its advocates" See http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/ for more information, also the verification working group: https://rust-lang-nursery.github.io/wg-verification/ https://rust-lang-nursery.github.io/wg-verification/
- grumblenum 5y ago
  I don't think that the mere existence of a "working group" or grant funded research positions for verifying rustc or a subset thereof is the same as having a verified compiler. That's certainly not a strong argument to against using rustc for safety over one of the many verified compilers that actually exist. At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist. Furthermore, that the proposed patches rely on the nightly compiler and a special variant of rust's core, which can only be enforced by special feature tags seems to suggest that Rust-Linux is not being written in this hypothetical, future compiler.
  - steveklabnik 5y ago
    It has not been done yet, it is a work in progress, but it is being done. https://ferrous-systems.com/blog/sealed-rust-the-pitch/ https://ferrous-systems.com/blog/sealed-rust-the-pitch/
    - grumblenum 5y ago
      My point is that solicitations for grant money do not provide the assurance that products that actually exist do.
      - steveklabnik 5y ago

kaba0 5y ago

Formal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.

hulitu 5y ago
Testing is hard. And (very) expensive.
- kaba0 5y ago
  Formal verification is even harder. And even more (very) expensive.
tonyarkles 5y ago
In a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons: - the requirements generally change quite frequently - the requirements are generally a long way from being "formally verifiable" Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work: - A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states. - A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases. - Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
- kaba0 5y ago
  Thanks for the informative answer! Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.
  - Y_Y 5y ago
    > TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.
    - kaba0 5y ago
      But it only proves a model, not the actual code — that’s a major distinction.
  - hwayne 5y ago
    It's formal verification of an abstract machine as opposed to running code. The problem is that formal methods as a field doesn't yet have a rich enough vocabulary to distinguish between its flavors. I use "code verification" and "design verification", which is a little more specific, but has its own issues. Is TLA+ a sandwich?
- mmis1000 5y ago
  You can't write a bug and nor can you write a test if you don't even have proper spec. But it happens a lot when requirements are just ambiguous.
grumblenum 5y ago
I was under the impression that SeL4 exists.
- raphlinus 5y ago
  Kinda. https://news.ycombinator.com/item?id=27232401 https://news.ycombinator.com/item?id=27232401 I think CSIRO disbanding the team was a huge mistake, but in any case they weren't producing the kind of success metrics that sustained their funding.
  - dnautics 5y ago
    I know of at least one other company that is picking it up.
- MaxBarraclough 5y ago
  That's true, but as a microkernel, seL4 has a very limited scope. It's not in the same ballpark as, say, the Linux kernel. It's more like a hypervisor. [0] From a quick google, seL4 has around 10,000 lines of C code, whereas the Linux kernel has around 30,000,000. [0] https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf
johnisgood 5y ago
https://github.com/Componolit https://github.com/Componolit Let us see what they have, using formal verification (Ada/SPARK). - JWX is a library for handling JSON data and more. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. As a result, JWX is particularly suited for processing untrusted information. - The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by Ada. A detailed description of the language elements can be found in the Language Reference. - Formally verified, bounded-stack XML library This is just Componolit. Let us check the F* language: - F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives. --- Given the above, what exactly do you mean that it does not scale?
- johnisgood 5y ago
  Whoops, I completely forgot about libsparkcrypto (https://github.com/Componolit/libsparkcrypto https://github.com/Componolit/libsparkcrypto) which is a "formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.". Features: * AES-128, AES-192, AES-256 * AES-CBC (all supported AES modes) * SHA-1 * HMAC-SHA1 * SHA-256, SHA-384, SHA-512 * HMAC-SHA-256, HMAC-SHA-384, HMAC-SHA-512 * PRF-HMAC-SHA-256, PRF-HMAC-SHA-384, PRF-HMAC-SHA-512 * RIPEMD-160 * HMAC-RIPEMD-160 * ECDSA, ECGDSA It is pretty awesome. :)
  - dexterlemmer 5y ago
    Looking at the examples you've provided, I'm pretty sure the Linux kernel's codebase dwarfs their combined codebases into insignificance. Since it is very hard to not have NP-hard asymptotic complexity when formally verifying a codebase as large and as demanding (in terms of performance, etc) as the Linux kernel, I would expect that if you tried to rewrite Linux in the languages you've mentioned and formally verify the rewrite, you will be able to keep the entire AWS cloud (globally) very busy for a very, very long time. On the other hand, if you were to do the rewrite in Rust and use some hypothetical formally verified Rust compiler to type check it (which is mathematically equivalent to such a formal verification in, say, F* limited to only verifying certain properties), it'll probably type check in minutes or even seconds on the laptop I'm currently writing this reply on. For a less hypothetical example. RedoxOS has a codebase that dwarfs Sel4 (but it is still much smaller than Linux in turn), yet it type checks with much less compute cost than it takes to formally verify Sel4. Or heck, Redleaf actually formally verifies in a tiny fraction of the time it takes to formally verify Sel4, because the Rust type checker not only significantly reduces the amount of requirements that still needs to be formally verified but also reduces the complexity to verify those requirements to linear to the codebase size due to the restrictions that the Rust type system and module system puts on valid Rust programs (with a little bit of care when writing the code). Of course, until you have a certified Rust compiler there might still be miscompiles of Redleaf and until all the features of Rust used in the Linux kernel is formally specified, we cannot do the same with the Linux kernel as for Redleaf even if somehow all of Linux got rewritten in Rust. But in Rust at least it is conceivably possible given sufficient resources and sufficient time. I very much doubt it will ever be possible without help from a sufficiently expressive and practical type system. Oh yea. Then there's another problem. Most (all?) of the examples you've mentioned have requirements that are well specified and pretty much set in stone. The requirements fro the Linux kernel... aren't quite as obliging.
dnautics 5y ago
Sel4 is an OS that is formally verified. It's security parameters are well-defined enough that you can use it to launch isolated VMs with... less secure OSes that are sandboxed from each other.

lmm 5y ago

Rust has far more enthusiasm from potential contributors than any of those options. Onboarding something is meaningless if it's not going to be used and maintained. FWIW I would trust anything language-level over applying static analysis tools to C (for an evolving codebase like Linux, having the safety be a first-class part of the codebase is a must) or extracting C from another language (the semantics of C are surprisingly weak, such an extraction can only ever be as good as your model of C which will probably be buggy).

zozbot234 5y ago

> I've never read anything to make me think that Rust is a safer alternative than any of these options What Rust focuses on is providing a scalable approach to a limited kind of formal verification - focusing purely on type- and memory-safety, not conformance to arbitrary specifications. The latter is of course being worked on, but type safety and memory safety are table stakes.

grumblenum 5y ago
> focusing purely on type- and memory-safety, not conformance to arbitrary specifications What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?
- zozbot234 5y ago
  Types are not 'arbitrary' in any real sense. Type systems can be described as a sort of formal verification that leverages and is closely aligned with the syntax structure of actual code, thus type systems can preserve compositionality but don't generally support non-local reasoning, at least not in a very elegant way. This is exactly what can make them potentially more scalable than other sorts of FV, hence more useful for programming "in the large".
  - grumblenum 5y ago
    Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.
    - PhaseLockk 5y ago
      Maybe I can try to explain the parent comment's point a different way. When saying that rust works on types and not on arbitrary specifications, I think he is saying that rust is more limited than languages that support arbitrary specifications. However, by making this tradeoff it achieves a reasonable degree of safety without incurring a ton of overhead. I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec. When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system. Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.

erk__ 5y ago

Its not like Microsoft does not work on that, they probably have a dozen different formally verified programming languages around at the moment. You already mentioned F*[0], but there is also Checked C[1], VCC[2], koka[3], dafny[4], Project Verona and probably some more that I am missing. The point being that they have clearly evaluated and have used F-Star for parts of the OS already. [0]: https://www.fstar-lang.org https://www.fstar-lang.org [1]: https://www.microsoft.com/en-us/research/project/checked-c/ https://www.microsoft.com/en-us/research/project/checked-c/ [2]: https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ https://www.microsoft.com/en-us/research/project/vcc-a-verif... [3]: https://github.com/koka-lang/koka https://github.com/koka-lang/koka [4]: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5]: https://www.microsoft.com/en-us/research/project/project-verona/ https://www.microsoft.com/en-us/research/project/project-ver...

ngrilly 5y ago

Static code analysis is not enough for C: https://t.co/Pbo4iHqEub https://t.co/Pbo4iHqEub

jsymolon 5y ago
no twitter https://sheas.blog/papers/The_Challenge_of_Using_C_in_Safety_Critical_Applications.pdf https://sheas.blog/papers/The_Challenge_of_Using_C_in_Safety...
- ngrilly 5y ago
  Apologies. I thought I pasted the original link but I was wrong. Thanks for fixing it.

deleted 5y ago

[deleted]

geofft 5y ago

As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it. I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work. Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust. I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem. If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!

pjmlp 5y ago
> What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. It does, just not the way most are used to it. Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {} However many type constructions in Ada do dynamic allocation by themselves, including on the stack. If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.
- tialaramex 5y ago
  > If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path. So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis. Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.

nonameiguess 5y ago

Without being an expert in either language, given what Ada is used for, I'm sure it offers at least all of the safety Rust offers and probably more. But Rust has a lot more going for it than safety. Maybe it shouldn't matter for kernel code, but the focus on developer "ergonomics," high-level functional constructs and pretty flexible pattern matching, supporting both ML-style and Algol-style syntax, very strong language-level tooling for building, testing, packaging, and generating documentation, plus the fact that the language itself is so well documented with great, accessible tutorials. There's a reason it keeps winning Stack Overflow's most loved language award every year. It's easy to learn for people coming from almost any kind of programming background, supportive of newbs, and equally well-suited for application-level and system-level development, so it ends up with pretty widespread appeal. So again, I don't know that any of this should matter for selecting what languages you're going to support in the kernel, but as a purely practical matter, it's a lot easier to ask contributors to use a language they already know and use elsewhere than it is to ask them to learn something new that they don't use anywhere else, which is what Ada and Idris and what not would be for most developers.

rkangel 5y ago

> I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates. Note that some formal verification work has been done on the guarantees that the borrow checked provides (which led to finding and fixing an edge case bug), so there is a little more concrete evidence that just the "assurances of its advocates" See http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/ for more information, also the verification working group: https://rust-lang-nursery.github.io/wg-verification/ https://rust-lang-nursery.github.io/wg-verification/

grumblenum 5y ago
I don't think that the mere existence of a "working group" or grant funded research positions for verifying rustc or a subset thereof is the same as having a verified compiler. That's certainly not a strong argument to against using rustc for safety over one of the many verified compilers that actually exist. At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist. Furthermore, that the proposed patches rely on the nightly compiler and a special variant of rust's core, which can only be enforced by special feature tags seems to suggest that Rust-Linux is not being written in this hypothetical, future compiler.
- steveklabnik 5y ago
  It has not been done yet, it is a work in progress, but it is being done. https://ferrous-systems.com/blog/sealed-rust-the-pitch/ https://ferrous-systems.com/blog/sealed-rust-the-pitch/
  - grumblenum 5y ago
    My point is that solicitations for grant money do not provide the assurance that products that actually exist do.
    - steveklabnik 5y ago