Search Mailing List Archives
[liberationtech] Programming language for anonymity network
hannes at mehnert.org
Tue Apr 22 11:48:27 PDT 2014
-----BEGIN PGP SIGNED MESSAGE-----
On 04/18/2014 10:26, Stevens Le Blond wrote:
> We are a team of researchers working on the design and
> implementation of a traffic-analysis resistant anonymity network
> and we would like to request your opinion regarding the choice of a
> programming language / environment. Here are the criteria:
I'm a researcher with some experience in formal methods
(http://itu.dk/people/hame) and also software development
(https://github.com/hannesm) in different kinds of programming languages.
> 1) Familiarity: The language should be familiar or easy to learn
> for most potential contributors, as we hope to build a diverse
> community that builds on and contributes to the code.
> 2) Maturity: The language implementation, tool chain and libraries
> should be mature enough to support a production system.
> 3) Language security: The language should minimize the risk of
> security relevant bugs like buffer overflows.
> 4) Security of runtime / tool chain: It should be hard to
> inconspicuously backdoor the tool chain and, if applicable,
> runtime environments.
I actually question whether your criteria is extensive enough.
Especially from crypto systems and anonymity systems, I'd want to have
a proper specification of the protocol, either by writing it in a
logic system or by using a declarative programming language.
In my experience, code with lots of shared mutable data (such as
object-oriented and imperative programming) tends to produce usable
applications quickly, but once you want to go
multi-core/multi-threaded or extend at points not thought upfront, the
code becomes messy and really hard to maintain. Thus I'd go for some
functional programming language where you write most of the time code
which does not mutate the heap.
Another piece of thought is this static typing vs dynamic typing.
While the latter produces prototypes quickly, the former results in
much more confidence that the application will actually do the right
thing (again, static typing is not a replacement for testing).
Your fourth point can be mitigated by a) two compilers to
cross-bootstrap [http://cm.bell-labs.com/who/ken/trust.html] and/or b)
formalised and small runtimes.
At the time being I'd suggest to look into OCaml/Haskell/Erlang or
Idris (if you need a really expressive type system), maybe write
specifications upfront in Coq/HOL/Lem. I don't see any reason these
days to use C/C++ or another unsafe macro-assembly language (and
currently develop a TLS stack in pure OCaml to run with openmirage.org
/ be used by nymote.org).
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (FreeBSD)
-----END PGP SIGNATURE-----
More information about the liberationtech