TLS/SSL implementation in Haskell
github.com
github.com
Many are saying that one problem with Haskell is that you can't eliminate side-channel attacks due to features of the language. I disagree. There is no common language better than Haskell at encoding invariants in the type system. One could, for example, implement a "biggishnum" library in Haskell using large but fixed size integers and constant-time operations.
Free monads are a powerful idea in Haskell[1]. They allow one to easily generalize "interpreters" over sequences of commands. In Haskell, more-so than any other language I've ever used, one can decouple execution from algorithm specification.
Free applicative functors generalize further[2]. They define a computational structure that must be fixed a priori. That is, by definition a free applicative functor cannot know the state of the data during its execution.
There are some problems with this. Applicative functors have an operation which can lift regular functions into it. That operation would have to be hidden, so that only a kernel was exposed that offered the ability to initialize data, and then perform computations upon it.
But it's possible to do this. It is actually not a radical idea to imagine this being done in Haskell. Making a library and a set of primitive operations that can be used by an end user safely, in provably constant time is possible.
[1] http://www.haskellforall.com/2012/06/you-could-have-invented... [2] http://paolocapriotti.com/assets/applicative.pdf
In C you could have made some 'safe buffer' struct together with some safe set of functions. But people didn't do that.
Exactly.
struct buffer
{
void* data;
size_t len;
};
void smemcpy(buffer* dst, buffer* src, size_t n)
{
if(dst->len < n || src->len < n)
abort();
memcpy(dst->data, src->data, n);
}
Buffer bugs in C don't come from the language, they come from the tendency of C programmers to value performance highly. "I just checked that the buffer is big enough, I don't need memcpy to waste cycles checking it again. I don't need that length variable sucking up memory when I know how big the buffer is." Except when you do.
Sure they do. For example, nothing in the Turing machine specification tells you how fast they are. Whether a given program will run on a Turing machine in a given amount of wall clock time is undefined.
Here's a real example with real machines. Suppose you have a program with two threads. The first thread computes data and puts it on a queue for the second thread, the second thread writes it to the filesystem. When the compute thread has computed all of the data, it sleeps for 10 seconds and then terminates the program without checking whether the write thread has actually completed writing all the data to the filesystem.
That results in undefined behavior in every real language I've ever heard of. Whether the data is all written depends on how fast the CPU is, how fast the filesystem is, what other programs are scheduled on the machine that compete for CPU and filesystem access at what priority, etc. Languages don't define any of those things so you have undefined behavior.
It reads the default symbol (see e.g. the description of a TM on Wikipedia). It's semantics are well-defined.
The semantics of TMs are well-defined. The semantics of C's "undefined behavior" is not well-defined.
This is false. All Turing Complete languages allow you to compute anything other Turing Complete languages allow you to compute, but that says nothing about encoding, or about interaction with the world. For an obvious encoding example, imagine you have a turning machine that can write only the symbols 0 and 2 to its tape. This is obviously Turing complete - it's isomorphic to a TM that writes 0 and 1, the TM doesn't care how the symbols are labelled. Now, if we ask it to encode 7 it has no trouble doing that in some encoding, but that can't ever be "111" on the tape.
When does it even make sense to partially mix byte-level representations of some data?
The buffer abstraction is necessary, but far from sufficient to build security-critical code. To do so, you also need to code in semantics somewhere, and buffers know zilch about the meaning of the data.
Incidentally, this is another reason that the language can't save you from yourself. Program termination is sometimes totally unreasonable, e.g. in real-time settings. And it's unreasonable regardless of the language. When an airplane falls out of the sky, you don't get to declare victory just because the reason it did was an uncaught out of bounds exception rather than a buffer overrun. In that context the programmer must explicitly handle the condition that the buffer is too small, regardless of the language, because "abnormal program termination" is not an acceptable outcome.
Moreover, the purpose of the above is to achieve the level of bounds checking that you get with the likes of Java. If you want to go beyond that then you need something more complicated -- maybe add separate variables to the buffer struct for buffer_len and data_len and then have different memcpy functions based on whether you want existing data in the buffer to be truncated. But there comes a point at which further complexity produces more confusion than safety.
> But there comes a point at which further complexity produces more confusion than safety.
Buffer is simply not the right abstraction for complex protocols, regardless of how "complex" operations you define.
The parsing and validation routine is where you need the buffer abstraction. If you make a mistake there then a copy function that won't let you read or write past the end of the buffer will mitigate the damage.
if(obj != null) {
obj.stuff = ...
}
There are also tools to help with it in the form of @NotNull, @Nullable, etc.
It's a completely different issue compared to actually accessing memory in an undefined way as you can in C. The bounds check you are replying to is manually creating something like that exception through the use of abort() while in java it is done always at the cost of some performance in exchange for safety.
Null is just a built-in final/sealed type(enum?) with a single value and no operations defined, like boolean is a type(enum?) with two values.
That, combined with proper type inference, would alleviate a large chunk of the boilerplate associated with statically typed languages in general, and Java in particular. (For how much Java is pushed as moving errors to compile time, there are an awful lot of things that fail only at run time that could be checked at compile time...)
Same thing with checked exceptions. A checked exception is really just an option - return foo or failure.
So while I love strong and static type systems, the issue at play here is memory safety - the very reason for why people still use C/C++ is the same reason for why Heartbleed happened.
Although I'd argue that a truly strong type system should also catch problems with pointers. The compiler should try to prove that any pointer access/arithmetic can or cannot cause undefined behavior - if it could cause undefined behavior, emit a compiler error, if it cannot prove that it won't cause undefined behavior, emit a warning and insert a runtime check.
(Still have the underlying "unsafe" functions. But group them into part of the standard library as an "unsafe" package.)
You have to use other people's code / language constructs which are underspecified and/or you don't have time to fully understand. Throw in versioning to the equation and now the problem is exponentially worse. This is why C code will always be full of memory vulns. Heartbleed is a very oversimplified example of the problems in C.
No you couldn't've. C is fundamentally unsafe language and people like you should stop pretending it isn't.
Discounting bad PHP, a huge majority of bugs are in C/C++ code. And "past popularity" isn't a good explanation, because a lot of the software is fairly recent.
So, the following isn't an opinion. It's simply a matter of observable fact. If you write in C/C++, you are far more likely to introduce security vulnerabilities than in other languages; therefore, unless there's a pressing reason to use these languages, don't.
And in the case of crypto code, one could argue that there is a very good reason to use C/C++: to prevent timing attacks.
Timing attacks work when code tries to be fast, taking shortcuts where possible. There's a reason we talk big-O instead of big-Theta: we gladly accept when an algorithm finishes early. This is, in this case, highly undesirable. Shortcuts are great, everywhere but crypto; not unlike recursion being great, unless it's embedded.
A language where every expression takes constant-time to compute seems like a solution. No short-circuiting, no variable runtimes. Don't use sorting algorithms like insertion/quicksort where best-case & worst-case are very different; use selection/merge where best-case = worst-case = average-case. Use constant-time hash functions. Caching is a very prevalent (and somewhat invisible) shortcut that needs to be solved (how can a language disable caching?).
Obviously this isn't fast but you can't have both.
Merge sort is still pretty fast. It isn't the fastest. But safe > fast when it comes to reliability and security.
That is, I don't think this exercise really shows what you think it does. Consider, if 90% of the software out there is in c/c++, and you had equal representation of language to vulnerability, then you would expect 90% of the vulnerabilities to be in c/c++. This would not mean that you are more likely to write bugs in those languages. In fact, unless I misunderstand, it would simply mean you are just as likely to have bugs there as otherwise.
Right?
1. A huge number of vulnerabilities affect C/C++ programs, almost all of which are memory based.
2. Memory-managed languages take care of this for you.
3. Therefore, C/C++ shouldn't be a default choice in domains where a managed language does just as well (a separate question).
Everything else is tangential.
But here are some reasons why your second paragraph is dangerously wrong (and why my claim was not as you characterize):
1. It only applies if we assume a uniform distribution of security effort across languages.
2. It only applies if we assume that c/c++ is being used for the same class of applications programs written in other languages, or that the applications have similar attack surfaces.
3. It only applies if we assume a uniform distribution of security effort over all code regardless of age.
and so on...
And also, 90% of code -- especially relatively recent code -- is not written in c/c++.
Especially if you follow that with the claim of "If you write in C/C++, you are far more likely to introduce security vulnerabilities than in other languages." In order for that claim to stick, you have to show not just that there are more CVEs against c/c++ than other languages, but that there is the same effort spent in attacking non c/c++ programs. Right? (Or, am I misreading a claim on that?)
Sure, if you reduce that to "memory vulnerabilities", it is a true statement. However, you did not make that reduction. As you point out in your counter #2, there are plenty of other vulnerabilities out there. What makes you think people are more likely to avoid those than they are memory vulnerabilities in c/c++?
As for the 90% of code not being c/c++, what is the point? Unless you can show that they receive the same level of attack as the c/c++, you can not really use that to claim that they are inherently more secure. Worse, your throwing of php under the bus just shows that recent languages don't do enough to prevent security mistakes.
Heaven help you if you throw in XSS and friends. Suddenly one of the darlings of the tech industry at the moment, javascript, is rocketing to the top of the list for security blunders.
In C having such a 'safe buffer' struct would require discipline from you, in Haskell that'd be the natural order of things.
I understand that many C programmers don't do it, mind you, but how is that different from a Haskell programmer not using the proper type for a certain operation?
> value :: ConstantTime Int
But how do I obtain an "Int" from that, since I know it somehow relates to an integer type? The answer is: you must ask the implementation of ConstantTime for the value, and if it doesn't want to give it to you, it doesn't have to. Constructors can be one way.
The library author could define a number of additional operations. These operations are privileged, being written as part of the library, they can actually inspect the inner data at any time. This is the "small core" that needs to be verified.
> addInt :: ConstantTime Int -> ConstantTime Int -> ConstantTime Int > subInt :: ConstantTime Int -> ConstantTime Int -> ConstantTime Int > mulInt :: ConstantTime Int -> ConstantTime Int -> ConstantTime Int > divInt :: ConstantTime Int -> ConstantTime Int -> ConstantTime Int
Then to compute something like Euler's formula one could write a function in terms of those functions.
> newtonsMethod :: ConstantTime Int -> ConstantTime Int > newtonsMethod = ...
And one can be certain that the laws that apply to `addInt` apply to `newtonsMethod`.
This composition has wonderful benefits because if there is no branching operation defined by the library, users cannot use branches inside ConstantTime. To serially apply addition, multiplication, etc, one can write in a sort of reverse polish notation:
> square :: ConstantTime Int -> ConstantTime Int > square input = mulInt input input
Using the multiplication operator, (*), would be illegal there. And that function, square, cannot inspect the value of input. Because it can't inspect the value, it can't make choices based on that value.
Whether that merits dumping the incredible amount of man hours that have gone into OpenSSL is debateable. I'd probably say it's worth fixing OpenSSL and trying to refactor it into a more provably sound system.
I still fail to see how this is fundamentally different from a similar approach in C (but maybe that's because I don't understand Haskell at all). In C you would define your ConstantTimeInt as a struct, and define a bunch of functions that operate on this struct. Using a + or * operator is also not defined for this struct. You'd have to use
csiAdd(const struct ConstantTimeInt *addend1, const struct ConstantTimeInt *addend2, struct ConstantTimeInt *res)
void square(const struct ConstantTimeInt *value,
struct ConstantTimeInt *result)
{
sleep(rand());
return multiply(value,value);
}
This is illegal Haskell:
square :: ConstantTime Int
-> ConstantTime Int
square = do
randomRIO (0,100) >>= threadDelay
return $ multiply value value
In your envisioning of a C ConstantTime library, you would never finish writing the library. If someone wanted to perform date arithmetic, you would have to implement that in your library and check it by hand and monitor it and maintain it. You could never let your guard down on any commit that would touch an ever-expanding body of code that would have to be rigorously checked to handle increasingly complex scenarios.
For example, to implement a constant time big (but fixed size) integer multiplication operation, you would not be able to trust that some other author's composition of your functions is safe purely by its type.
For example, C is full of operations (pointer arithmetic, read from an unbounded array) that may read the inside of that struct without that code mentioning that struct in any way.
There are a few uncommon dependently typed ones with code extraction to other languages though. Though doing so is fairly time intensive still.
Ok, but if it were vetted as much as openssl, it would probably be much better, yes?
It probably would be slower though, which is kind of a big deal for webservers and the like.
More critically, it would only be useful to Haskell code. Haskell, unless C, cannot be embedded. Having a version in Rust - which does not rely on the runtime - ought to be safe from this kind of issue (baring any problem in Rust itself) while being still embeddable from external code. It would still be somewhat slower than C, and of course Rust is far from mature.
(Shameless plug) I've collected examples of this here: https://github.com/drdaeman/haskell-library-ffi-example
Why do you disagree?
Timing attacks are probably the easiest kind of side channel attacks to prevent but CPU cache line eviction and branch prediction are a lot more difficult to deal with. Especially when using a programming language with managed memory where you can't be quite sure what kind of memory accesses a program will perform. And in the days of virtual machines on cloud servers, they are very relevant.
I do not think that it is totally impossible to write Haskell crypto code without any side channels, it is certainly more difficult than writing crypto code in C or Assembler.
But the big problem is that now you'd need the programmers dealing with crypto not only to be proficient cryptographers but also experts on the internals of the Haskell runtime system. That's a pretty tall order.
I would like to hear from the original authors of this library, what was their motivation in starting this project? I am sure they were not unaware of the potential of side channel attacks. I don't think this project was started with the intention of replacing OpenSSL in production use, but perhaps for fun or educational purposes. Or perhaps to write offline tools for creating and validating certificates, etc.
This is amazing, because I mean truly fixed. The course of execution cannot be altered by the values of the input. Cache line eviction? All memory access is statically known in advance. Branch prediction? There are no branches.
The code would look a lot like what the Haxl[1] project at Facebook has produced. They used applicative functors to create a domain-specific language that described the shape of a computation without specifying the details. That allows them to write a compiler for their DSL in Haskell. In their case, they used Haxl to hide concurrency from their users, Facebook developers. Those developers can use Haxl to write concurrent, cached, optimized and type-checked queries against Facebook's datastores, without having to know how to write safe concurrent, fast queries. To the Facebook developers, there is no concurrency, the code they write just looks like a monad or an applicative in Haskell.
It should be no surprise then that one of the lead developers of Haxl originally worked on the Glasgow Haskell Compiler.
[1] Haxl slides [PDF warning]: https://github.com/meiersi/HaskellerZ/raw/master/meetups/201...
This might be what it looks like before GHC had its way with it. After GHC inlining, optimization passes, rewrite rules, the code may well contain branches, conditional memory accesses, etc.
This isn't a dig at either Haskell or C; the point is that all programming languages and environments have their "gotcha!" moments.
At this point, gcc and clang should at least provide constant time memcmp primitives; any custom solution not supported by the compiler is not portable and needs to be validated separately for each implementation, each platform, each compiler version.
Timing attacks is the first thing I thought of when I saw this implementation so this should be interesting if he can respond.
Getting around timing attacks is not too different in Haskell from doing the same thing in C. First, there's 2 different classes of timing issues:
1) cryptographic ones
2) and the others (for the lack of better classification)
For cryptographic ones, it's hard to enumerate all the counter measures used/not used, but some examples:
- use of blinding with RSA
- with ghc 7.8, exponiantiation is using GMP expmod_safe
- AES is using native instruction when possible.
- Use of scrubbed memory/memory constant where possible
- some lowlevel cryptographic implementations are actually in C (hash, aes, ..)
Also, while I'm linking against specific set of cryptographic implementations by default, there's nothing preventing anyone from pulling different crypto implementations from other places.
For the other issues, it's usually just a deal of strictness, and not bailing/notifying error too early. (e.g. This is what Bleinchenbacher and CRIME are all about).
- data comparaison is time constant by comparing all bytes where necessary: prevent padding attack
- there's routines to evaluate boolean values without bailing too early (False && ... -> would bail at the first false)
- lots of part in tls is using strict bytestring, and strict values.
- the GC is adding a lot of noise potentially hiding timing issues, potentially exacerbated by pure values instead of mutable values (like you would in C)
Also, I don't want to claim there's no issues or ever will be. Hopefully there's no such things, but I welcome any audits and questions about stuff that look fishy. But people shouldn't only looks at the cryptographic side of security; openssl had so many issues about basic unchecked values, buffer underflow, overflow that's not even funny anymore. Just sayin'
Likely this work would be necessary to "prove" (not in the strict form) your assumptions about constant-time anyway.
I don't think that laziness makes things much harder. Compare a C function with if foo return 0 in the middle and a Haskell function that lazily builds thunks that don't end up being evaluated in a particular branch. There's obvious things to do to both to make them run in constant time. The hard part about dealing with a timing attack in both cases is recognising that the function is used in such a context and needs to be constant time.
AFAIK, the haskell TLS stack has not yet been audited. For this reason, there's some reluctance to use it in parts of the Haskell community. Although http-conduit and http-client-tls do use it, so everyone writing programs that hit https from haskell using conduit is using it already.
As far as I understand, this is not sufficient.
Some things that are needed in addition are (at least):
* constant time math operations (multiply, divide, exponentiation, etc.)
* no branching based on secrets (running the code results in no branch conditions based on secret data)
Here's an interesting article on implementing a form of Elliptic Curve Cryptography without even local timing attacks: http://blog.cr.yp.to/20140323-ecdsa.html
cryptofunc x = do
begintime <- gettime
result <- purecryptofunc x
endtime <- gettime
sleep (worstcase - (endtime - begintime))
return resultTime to sleep() would vary across processors, os-es, and even load (!), so it's not exactly a workable solution. Not to mention it would be grossly inefficient (Context switch on every crypto primitive? No thanks).
It also seems reasonable to add a random length of time to the sleep time, so that differences in computation time are indistinguisable from the randomness added by the random variable. I could be completely wrong though.
(also, you probably need to force with seq or deepseq the result of purecryptofunc before getting the second time, or you might be adding that evaluation time to another part of the code, and then this code becomes just a constant time added to the computation)
> The software implementation uses S-Boxes, which might suffer for cache timing issues. However do notes that most other known software implementations, including very popular one (openssl, gnutls) also uses similar implementation.
Oh, well if OpenSSL does it..
http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/bang-...
(The similarly looking BangPatterns extension is supported by GHC only.)
This whole thing has got me curious about techniques for formally verifying software.
I'm a complete beginner on this topic, but I assume there are tools to help write software that's formally verified / proven to be correct. Can they make any guarantees about side-channel aspects such as timing in these systems? Anyone care to give me some pointers on where to begin?
A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ for it though.
The challenge comes in when you try to translate. You write your model up and validate your approach, you then try to translate it into C (or whatever) and that point you can be as certain of your design as you like, you still can't be sure that the compiled software will work properly. I haven't seen a convincing solution to that particular problem (and I've done some research on the topic for three separate projects now).
There's two reasons for this... first, a pure-Haskell solution locks it to Haskell only, as there's very little realistic chance of embedding Haskell in any other environment. Having it compile to something like straight assembler or LLVM means that we can almost certainly wrap that in almost any runtime environment effectively. (We might require a bit of new SWIG-like tech to do it, but under the circumstances it would probably be worth it.) To the extent that's not a true statement, imagine that I will research and find the correct level of abstraction. (Maybe it really is C.)
Second, with all due respect to the Haskell runtimes in the world, it's just too big a surface to secure. People are asserting here in this thread that you could avoid side-channel attacks in the Haskell runtime, but how would you prove that? To any degree?
Theoretically, you might be even better off in a real proof language, but it's not clear to me that any of them have a good enough extraction-to-LLVM/assembler story.
This would, in theory, produce a solution that should be embeddable in nearly any other language, and indeed, even in embedded environments, while still leveraging the strengths of Haskell's expressiveness and type safety to build a very safety-critical library. We would also be able to write some powerful tests to verify that the putative time-invariant operations really are time-invariant. My strong suspicion is that we'd discover some processor differences here that would surprise everybody.
However, this says nothing about whether or not the implementation is secure. They admit that they don't model time in their proofs, so I doubt their implementation is free of timing attacks. Moreover, its written in F#, so you have to trust your CLI implementation to be bug-free as well.
Is that any different to an implementation in C relying on the processor being bug-free?
The number of states and transitions for a processor today is large, but not so large that engineers can't formally and automatically verify that the processor will behave correctly under all inputs. Also, the structure of the processor and the way it is specified (i.e. Verilog) make it amenable to formal verification.
This is not true for most software, not even things written in Haskell. You can cover a lot of cases with automated software testing, but you'll find that it's very, very, VERY hard to prove that you've covered every possible case. Even if you can, modeling multiple instances of the system as they evolve in time (i.e. any networked system or interactive system) means you have to consider all possible combinations of states they can be in.
To put into perspective how hard formal verification of software is, I have a story. A friend of mine did his masters thesis on modifying TCP to allow for host mobility, and formally proving the correctness of his new TCP protocol. Despite having a 100-node cluster of beefy (48GB RAM) compute nodes at his disposal, it simply didn't have enough total RAM to verify the correctness of his protocol beyond five rounds of communication between one client and one server.
Unless the CLI developers add machine-checked but hand-crafted proofs of correctness for each and every method, I trust the processor to be bug-free far more than any piece of software it runs. Now of course, if the NSA tampers with either, then all bets are off :P
I'm completely ignorant about Haskell. I see there's some code in a "Benchmarks" folder; I think it would be highly interesting to see a comparison in speed between OpenSSL's SSL implementation and this one (the operations that a web server would normally have to do).
Can anyone make that happen? I can't even figure out how to execute Haskell code in Ubuntu 13.04.
Seems to me like if the code base is 20 times smaller than OpenSSL, and we can assess whether timing attacks are present or not -- and if they are, replace the timing critical code with C code, perhaps -- that this would be a real alternative to OpenSSL. Am I being unrealistic in thinking this? Not that everyone will adopt it, mind you, but that adopting it would be a wise thing to do?
sudo apt-get install haskell-platform
On one hand, it is a very high performance language with tons of purity, abstraction, and invariants built in to the type system and semantics. On the other hand, certain aspects can be problematic to reason about.
E: Unable to locate package haskell-platform
A bit of research shows that it's possible to make shared libraries with haskell, but not quite as straightforward to use them. I have no practical experience about how troublesome it would actually be.
http://packdeps.haskellers.com/reverse/tls
Meanwhile, HsOpenSSL (Haskell bindings for OpenSSL) has 22 dependencies:
On the other hand, I undoubtedly agree that we should start making and deploying alternatives in more safe modern languages. In fact, I guess we should start step-by-step rewriting everything that's written in C/C++ and OpenSSL is a good thing to start with.
I guess it's a good chance for Rust & friends.
Can Rust compile to a shared lib the programs can use as easily as a C library? (I think the answer is "not yet", but I'm not sure? At least, I've seen projects for compiling Rust without any runtime library).
Today I learned this is possible with Ada [2], but it seems there is some boilerplate to start/stop the runtime. Does Ada provide the necessary low-level control to implement crypto?
Are there sufficiently strict dialects of C?
NaCl [1] says "There are an increasing number of cases where the C implementations and assembly-language implementations are automatically generated from code that was actually written in another language, such as CAO or qhasm."
CAO is a "a domain specific language for describing cryptographic software" [3], while qhasm [4] is a portable assembly seemingly not focused on safety.
[1] http://nacl.cr.yp.to/internals.html
[2] http://gcc.gnu.org/onlinedocs/gcc-3.4.3/gnat_ugn_unw/Creatin...
[3] [PDF] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.113...
Yes it can! You use the `#[no_std]` if you wish to be rid of the runtime, and the `#[crate_type = "lib"]` for outputting shared libraries (or use the `--crate-type` compiler flag).
Here's an older blog post on it, though the rust code there probably won't compile as-is with current Rust: http://bluishcoder.co.nz/2013/08/08/linking_and_calling_rust...
https://github.com/thestinger/rust-core
Right now, rust-core only provides basic collections and io, but more may be in the works. I suspect rust-core will eventually grow into a small but capable standard library.
Instead, the Rust devs intend to restructure the standard library such that it has multiple profiles, and that you can jettison parts of it (such as the parts that require the runtime) without losing all of the other goodies. Here's the most recent RFC for doing so, filed yesterday: https://github.com/rust-lang/rfcs/pull/40/files
#![crate_id="basic_lib"]
#![crate_type="dylib"] // for a .so
/* not there's no `no_std` */
#[no_mangle]
pub extern "C" fn add_in_rust(x: i32, y: i32) -> i32 {
x + y
}
There are many functions/types in libstd etc. that can be used without a runtime (although its still not as great as it will be in future).
When you start to worry about compiler bugs, hand written macro assembly isn't such a crazy idea for algorithms like SHA, MD5, RC4, AES. It is also easier to reason about timing in assembly. The truly paranoid would have to check compiler output anyways.
You also get the powerful feature of pre and post conditions being part of the language from Ada 2012 onwards, meaning you can even more precisely control what's happening. You can have types for potentially dangerous data and safe data that cannot be intermixed without being very explicit about it (something that would've avoided this bug if I understand it correctly).
I've said it in other threads, and it's worth saying again (as someone whose primary language is Haskell) Ada is absolutely the right choice for this sort of programming. It's just as low level, if not more so, as C, with all the high level constructs of C++ (well most anyway), it encourages writing safe code by making the safe easy and the unsafe hard, and has excellent open source tools backed by commercial compiler writers (AdaCore).
And the last, but not the least, timing attacks aren't chief vulnerability, really. If you expect a timing attack being real hazard you can randomize return time explicitly.
I am still a (interested) Haskell beginner but whenever this discussion comes up the first thing I think is "why not try this in Haskell?" and I never give a thought that I would do this in Java which is my everyday language (and reasonably memory safe).
Not true. It's long been known that timing attacks over a LAN are practical (replace LAN with intra-datacenter network). Relevant paper from 2003: https://crypto.stanford.edu/~dabo/papers/ssl-timing.pdf
It isn't just accidental errors you need to worry about. Obfuscated intentional errors are a problem too. If the language design prevents bugs that an NSA mole would try to slip in, then that is a very good reason to rewrite in a new language.
Minor edit: almost four years
Could you elaborate more on this? I fail to see how this is inevitable.
Something with a bit more ML in its blood would be better, and for a library that pretty much means OCaml.
Edit: I do not at all mean to imply that it is impossible to implement TLS securely in Haskell. Only that there are more natural choices if one wants the advantage of a strong algebraic type system.
The classic example of this is checking string equality with strncmp(): this takes a different amount of time depending on how similar the strings are. If one string is secret and the other is controlled by an attacker, the attacker can use a clock and multiple attempts to discover the secret.
Obviously this particular one isn't relevant to SSL, but there are a number of other possibilities to worry about in most languages, most obviously short-circuiting operations like boolean AND/OR. Lazy evaluation makes every operation short-circuit, so you need to worry about this in every operation.
It can be done, but it's harder than it needs to be.
We could use something that gives both advantages, like the OCaml I already mentioned. Or, we could take a hybrid approach, where something like Haskell generates C code that provably can't have buffer problems. Or, we could statically verify that the library is written in a known-memory-safe subset of C++. Or, we could use a language like Rust, which (once it's eventually complete) seems ideal for this sort of application.
Here's an example of a type definition that specifies strict evaluation https://github.com/vincenthz/hs-tls/blob/master/core/Network...
See? They don't have to switch languages after all.
Seriously, for many languages bugs cause unintended behavior within bounds of implemented logic - such as the recent logic bug that returned an 'okay' response even if the certificate was invalid; however, the fact that ordinary bugs tend to have effects of "read arbitrary memory" or "execute arbitrary code" is a very specific niche of C and friends.
In a language appropriate for security, a bug in heartbeat extension would break the heartbeat extension - maybe disable heartbeats not work, maybe cause different heartbeats - but it should be unable to affect the rest of application. In a language appropriate for security, if a single module is secure (i.e., the limited number of API/method calls it exposes are secure), then bugs in all other modules shouldn't be able to affect the insides of that module; so if your app has a tiny core that does some signing w/o exposing the key secrets, then the rest of the app can't touch it even deliberately, much less by an acidental bug.
Go is probably better at this.
(Also, he's one of Google's point people on TLS.)
JFWIW.
Why? Go doesn't really offer a whole lot in terms of security, except for better managed memory. I'm not even sure you could reliably eliminate side channel attacks in Go.
What makes it better? Haskell's GC is very advanced.
Better than C, that is. Haskell is on a whole 'nother level of "what are memory bugs?"
http://hackage.haskell.org/package/base-4.7.0.0/docs/Foreign...
Bad. They are not something to blow off. They may seem "out there", but they are actually leveraged somewhat frequently. They are particularly dangerous in certain shared-hardware environments (e.g. VPS services like DigitalOceal, AWS, etc), and against physical devices that are supposed to resist data extraction (like smart cards).
It sounds like lots of people (sockpuppet echo chamber) are saying if the new language/runtime doesn't fix all possible flaws we should stay with the broken-on-purpose OpenSSL codebase?
I think it's more likely they are saying that replacing one broken implementation with another broken implementation isn't worth the effort.
Sure, remote code execution and reading of arbitrary memory are a lot worse than an attacker figuring out a private key. But if an implementation of a crypto system is not able to conceal the private key, it is completely useless.
Seems to me like we may need to, first of all, redesign some algorithms to be easier to implement in constant time (like Ed25519 and symmetric encryption algorithms that avoid S-boxes), and secondly, develop a language that combines both memory safety and the ability to reason about whether an operation runs in constant time.
I'm not saying this is something we just do, it's a huge undertaking. I'm saying that it seems to me this may be needed, unless we want to find 5 years down the line, when everyone is using a Haskell TLS implementation, that attackers can retrieve the private key through timing attacks. That would be a fairly large effort put towards writing another TLS implementation that is broken by design.
Here are all the current TLS implementations http://en.wikipedia.org/wiki/Comparison_of_TLS_implementatio...
There is room for one in a secure language.
Completely useless? Go ahead and throw the baby out with the bathwater. At this point OpenSSL is a net negative.
It really smells like you are spreading FUD to keep people on OpenSSL.
Reasoning about a smaller code base is nonlinearly easier. This is especially important for security software where letting your reasoning slip usually renders the whole thing useless.
Not so much for Haskell. When I started with it, I similarly tried to learn by going through the language libraries. Even when I gained some more experience (I am still a beginner and only casual user, though) I have a very hard time to understand what's going on. The code is so dense that I find it hard to understand.
Seriously, the Haskell libraries are understandable and informative - once you learn the language.
I have casual encounters with Haskell since two years now. Library code is still hard to grok. Don't get me wrong: I like Haskell very much and I am pretty sure that its a decent language to write security critical code in, but I think this is still a problem for many beginners out there. I very rarely stumble on something and say: "hey, that's cool, I will use that in my code". But I admit that I give up after the third nested "lift-<whatever>" ;-).
I want the libraries help me understanding the language, not vice versa. But of course, that's not their primary goal.
A direct analogy to what you're saying: When I was studying French, I was able to read articles above my level and get a decently good idea of what they said. Now I'm studying Chinese, and I can't tell at all what characters mean! This should not be surprising. French is very similar to English, where Chinese is very different. Of course picking things up in the latter will be more difficult. It would be absolutely absurd to blame the Chinese language for that.
I agree.
The effect could be offset by having to reason about the implementation details of a more complex platform though.