3 ms·

What would be a better language for creating a small, portable crypto library that works on embedded systems? Would you really put your trust in a brand new lan

by seibelj 10y ago

What would be a better language for creating a small, portable crypto library that works on embedded systems? Would you really put your trust in a brand new language?

banach 10y ago
Given that this is a reasonably small code base (compared to, say, an OS kernel), an idea would be to use a language that provides strong guarantees about correctness the implementation. For example, Spark Ada can be used to do that. Alternatively, keeping the implementation in C, a similar level of assurance could be achieved by developing the library along with a specification, and requiring any extensions to pass some kind of correctness proof based on this specification.
- pjmlp 10y ago
  The is approach taken by the F* folks on their TLS library.
pornin 10y ago
Actually, C is a horrible language in many respects, but it is also the only language that can achieve any kind of decent compatibility in embedded systems, which is why I used it. Also, when I say that BearSSL is written in C, it is partly a lie: some of it (especially X.509 certificate decoding, and handling of handshake messages) is done in T0, a new Forth-like language that I invented for the task (compiler is provided, and produces C code), specifically to have coroutines (incidentally, it means that most of that code read things byte by byte, with relatively few accesses to buffers, thus less potential buffer overflows).
- stompin 10y ago
  do you really need coroutines for cert decoding and handling of handshake messages? It's not like you can parallelize these things and do something else in the meantime...
  - pornin 10y ago
    Certificates and handshake messages are nested structures, and I want to process them in a streamed fashion (e.g. I don't buffer a complete certificate, I don't have the RAM for that; BearSSL can decode certificates and messages that are larger than the total RAM is uses), so without coroutines, I would still need some sort of decoder with a stack of states, so I just accepted it and pushed the idea to its logical conclusion. Despite the horrors implied by a Forth syntax, this actually made writing the code easier. As a bonus, it turns out that T0-generated code is very compact, so I could pack more behaviour into less bytes.
- seibelj 10y ago
  Thanks for your response! I'm going to shoot you an email, I would be interested in helping you with this project.
- unwind 10y ago
  Here's a link to the first T0 code I found, for the interested readers out there: https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/x509/x509_minimal.t0;h=bdb3e18c6ad47840e758cb3a3340d6383c1bb590;hb=3210f38e0491b39aec1ef419cb4114e9483089fb#l418 https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/x509/x509....

by seibelj 10y ago

What would be a better language for creating a small, portable crypto library that works on embedded systems? Would you really put your trust in a brand new language?

banach 10y ago

Given that this is a reasonably small code base (compared to, say, an OS kernel), an idea would be to use a language that provides strong guarantees about correctness the implementation. For example, Spark Ada can be used to do that. Alternatively, keeping the implementation in C, a similar level of assurance could be achieved by developing the library along with a specification, and requiring any extensions to pass some kind of correctness proof based on this specification.

pjmlp 10y ago
The is approach taken by the F* folks on their TLS library.

pornin 10y ago

Actually, C is a horrible language in many respects, but it is also the only language that can achieve any kind of decent compatibility in embedded systems, which is why I used it. Also, when I say that BearSSL is written in C, it is partly a lie: some of it (especially X.509 certificate decoding, and handling of handshake messages) is done in T0, a new Forth-like language that I invented for the task (compiler is provided, and produces C code), specifically to have coroutines (incidentally, it means that most of that code read things byte by byte, with relatively few accesses to buffers, thus less potential buffer overflows).

stompin 10y ago
do you really need coroutines for cert decoding and handling of handshake messages? It's not like you can parallelize these things and do something else in the meantime...
- pornin 10y ago
  Certificates and handshake messages are nested structures, and I want to process them in a streamed fashion (e.g. I don't buffer a complete certificate, I don't have the RAM for that; BearSSL can decode certificates and messages that are larger than the total RAM is uses), so without coroutines, I would still need some sort of decoder with a stack of states, so I just accepted it and pushed the idea to its logical conclusion. Despite the horrors implied by a Forth syntax, this actually made writing the code easier. As a bonus, it turns out that T0-generated code is very compact, so I could pack more behaviour into less bytes.
seibelj 10y ago
Thanks for your response! I'm going to shoot you an email, I would be interested in helping you with this project.
unwind 10y ago
Here's a link to the first T0 code I found, for the interested readers out there: https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/x509/x509_minimal.t0;h=bdb3e18c6ad47840e758cb3a3340d6383c1bb590;hb=3210f38e0491b39aec1ef419cb4114e9483089fb#l418 https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/x509/x509....