So far I mostly saw Python (because of simplicity) and C (because of efficiency) for cryptographic programming. But there is a different kind of programming languages called functional programming languages. An example is Haskell. These languages have no side effects and can be proven correct. I was wondering if those programming languages would have any benefits over "normal" programming languages when used for cryptographic applications. Is that the case? If yes, why aren't they used more frequently?
$\begingroup$
$\endgroup$
4
-
1$\begingroup$ The real only problem is that your programs if done right might become so intuitive and easy to understand and maintain in the future that anyone will easily understand what you ate doing and crypto will not be a hard field in the end. But leaving aside the melodrama, if done right it will bring clarity to your code and will help you do more with less lines of code. $\endgroup$– Roman GhertaMay 21, 2021 at 8:29
-
7$\begingroup$ I think that the fact that functional languages are often more concise doesn't always help with regards to clarity. Fact is, many developers will find functional constructs much more abstract and harder to understand that a swath of well written code that does what you tell it to do. $\endgroup$– Maarten Bodewes ♦May 21, 2021 at 10:46
-
3$\begingroup$ There is a functional programming language called Cryptol that's specialized for cryptography, but as far as I understand it, it's mostly for specification and analysis cryptographic designs, and not really for practical implementations thereof. $\endgroup$– Luis CasillasMay 21, 2021 at 22:35
-
1$\begingroup$ ’have no side effects’ No, they can have side effects, whether a function is pure or not is a property of the function, not the language (you can write pure functions in Python just fine). Same for provable correctness, that’s doable with other languages too. $\endgroup$– Austin HemmelgarnMay 22, 2021 at 22:48
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
4
These languages have no side effects
Well, yes, kind of. They also are higher level languages, where you don't have (as much) control over e.g. timing or the wiping of memory. Those are the side effects that cryptographers worry about - rather than the mathematical side effects that you are alluding to.
I was wondering if those programming languages would have any benefits over "normal" programming languages when used for cryptographic applications.
Personally I think that any higher level language that provides e.g. memory protection is really a requirement for a secure application. Those kind of memory protection is generally provided by functional languages. It is probably even better than higher languages where you may have mutable variable values.
However, for the cryptographic primitives it makes sense to use machine code and - of course - native instructions whenever they are available. I've seen that bit-ops are generally much slower on these kind of languages. And we're talking about huge numbers here. For instance, Java and C# are already much slower than C if cryptographic primitives are programmed correctly (think a change of 2 x in performance degradation). Most other interpreted languages are much slower than that.
The performance advantages that functional languages may bring - such as delayed execution by passing functions - are not helpful - if not outright dangerous - for cryptographic primitives.
I was wondering if those programming languages would have any benefits over "normal" programming languages when used for cryptographic applications. Is that the case? If yes, why aren't they used more frequently?
Here again we must make a distinction between "cryptographic applications" and "cryptographic primitives". I think that a well tested library of native functions is quite often used within higher level languages. There are e.g. many OpenSSL wrapper libraries in use within higher level languages such as Python. I think this makes sense, although more (array) boundary testing on the used native libraries would be useful.
As for functional languages: I don't see this "proven correctness" as much of a benefit. Unusually there some boundary checks etc. to be made. But otherwise, generally you can work with the test vectors to show enough correctness for the primitive.
I still see purely functional languages mainly useful for mathematical applications and such like. Personally I think that they are complex enough that most developers will not use them for generic applications. Those kind of mathematical applications are generally not the type of applications that require a lot of security.
Whatever you think of the last section (which is rather opinionated), generally we don't choose a language based on the cryptography we tend to use. Security should be an integral part of an application design, but usually it is not the main use case. A language is mainly chosen because it fits the main use case or - of course - simply because of developer familiarity (and purely functional languages still are not the most popular languages out there).
answered May 21, 2021 at 10:16
-
3$\begingroup$ I don't see this "proven correctness" as much of a benefit. -- indeed, this concern comes when you're dealing with a new algorithm you might not have even thought of all the corner cases on (thus, you hope they all come out during your "proof" stage). current crypto algorithms simply don't have ambiguities like that left; there's no wiggle-room left which you would need a proof to help you tease out. $\endgroup$ May 21, 2021 at 19:52
-
1$\begingroup$ Note that there are much lower level languages that still have very good protection against memory related errors, like Rust. $\endgroup$ May 22, 2021 at 3:52
-
$\begingroup$ Yes, fortunately there has been at least some effort spent towards security. Unfortunately the static (source) code analysis did not make as much of an impact as I suspected and the C language in particular is still vulnerable against buffer overruns and such. $\endgroup$– Maarten Bodewes ♦May 22, 2021 at 12:36
-
3$\begingroup$ The idea that cryptographic primitives implementations should not be proven correct is quite false, as subtle implementation bugs do happen, see e.g. people.csail.mit.edu/nickolai/papers/lazar-cryptobugs.pdf. Recent work has been done on verification: github.com/mit-plv/fiat-crypto. Used in Chromium I believe! $\endgroup$– codyMay 23, 2021 at 3:45
$\begingroup$
$\endgroup$
Functional programming languages are typically strongly typed. This makes it impossible to commit a wide class of errors when implementing cryptographic algorithms. For example, if a cryptographic key is declared as having type Word32 in Haskell, then it is impossible to add it to a plaintext of type Integer (unbounded size): the code will be rejected by the compiler at an early stage after it fails to type check.
More impressively there is the domain specific programming language Cryptol built on top of Haskell that extends the type system to allow very precise specifications of cryptographic algorithms. For example, on the main page of the Cryptol website the SHA-1 hash function is defined, with type signature
f : ([8], [32], [32], [32]) -> [32]
indicating that the $t$-th step of SHA-1 is a function $f_t$ taking three 32-bit words and returning a new 32-bit word. From the [8] we know there are at most 256 steps. (In fact there are 80.) Of course this is only the type signature, but the implementation is similarly concise.
$\begingroup$
$\endgroup$
4
"Proven correct" was all the rage in the 70s and 80s. It is basically dead and discredited, living on only in theoretical computer science. The problem was not technical, but was a fundamental conceptual failure which should have been obvious.
The first problem with "proven correct" is defining what "correct" looks like. This can only be done by writing the algorithm - in short, by writing a program. So you define one program as "correct" by whether it matches a second program. How do you know the second one is correct? Answer: you don't.
The modern answer to this is testing. We know (and we have evidence) that high-quality testing which includes corner cases is highly likely to find coding errors. We can't prove there are no bugs, but we can put decent statistical limits on it.
And the deeper problem following this is "did we get the right definition of what we should consider correct?" In practise we now know that most serious failures don't usually come from coding errors, they come from incorrect specifications. Formal proof would only provide proof that the program does what was specified, not that it achieves what was intended. Only testing can confirm this, and acceptable testing may often need to be qualitative ("does it feel fast enough?") and not quantitative ("does it run this in under 100ms?").
-
4$\begingroup$ This is incorrect. Actually, "proven correct" is more popular now than ever, under the term "formally verified". At the moment, there are several microkernels that are fully or partially formally verified (such as seL4 for MMU systems and Chronos or whatever it's called for non-MMU systems, and some proprietary microkernels for aerospace applicatoins as well). There are some formally verified libraries (like miTLS), and some components of Windows are formally verified as well. $\endgroup$– forest ♦May 21, 2021 at 22:58
-
$\begingroup$ @forest Except that the method used to verify is most often exhaustive testing. This is the logical conclusion of testing as I described, and rejecting the concept of mathematical proofs. Having worked in safety-related and aerospace myself, formal proofs really weren't on anyone's radar - what happens is formal testing and lots of it. And requirements capture and traceability, of course. $\endgroup$– GrahamMay 22, 2021 at 1:29
-
3$\begingroup$ You're right that testing is the primary thing to do even for high-assurance ratings like EAL6, but formal verification itself is not just based on testing, but mathematical proofs of correctness. Most likely the work you did was kept out of the TCB, which is why expensive and time-consuming formal verification wasn't a thing. For things like microkernels that are in the TCB, formal verification is very much alive. If you work on anything above EAL5, you'll be doing some formal verification. With mathematics. $\endgroup$– forest ♦May 22, 2021 at 1:30
-
$\begingroup$ There was definitely a lot of hype in the 1980s which fortunately faded. But -- the same can be said about functional programming itself. The hype was misplaced, but as the theory and the technology matures, things which were purely theoretical can become more practical. Almost nobody used functional programming outside of academia for decades -- until Ericcson invented Erlang for use in telecommunications. It is doubtful that formal methods will ever live up to their original hype, but it is an exaggeration in the other direction to call them "dead and discredited". $\endgroup$ May 22, 2021 at 12:15