Hello, hi, hello, I'm Siza, I'm a newcomer from the Aida and Spark community and the
ecosystem and I have been studying cryptography and cyber security and so that's what inspired
me to write a big integer library for cryptography in Spark.
So when we need a constant timer, cryptography printed like big integers, we need them to
avoid some side channels in cryptography code and I wanted to be able to provide some
strong creatives for building stuff in Aida.
So yeah, I wrote a big integer library in Spark with designs and algorithm that were
inspired by Rust CryptoBigintCrate and all the functions that I wrote are in constant
time explicitly named as search, but yeah, it's still some experimental code so I would
advise to use it in some security sensitive context.
But what I've been talking about constant time since the beginning, but what does it
actually mean in a context of big integers?
A constant timer algorithm is an algorithm that will not have dependencies in terms of
resources on secret values and values that we want to remain private.
So it will not leak data depending on the, depending on branches on memory accesses or
timing data and all the operations that you can do on those structures are always take
the same time in the same resources.
So we have no branching on secret values, we have no memory accesses that depend on secret
values to avoid leaks due to cache access latency and such things.
And for instance, there's a famous kind of famous vulnerability in some area say code that
would leak some information about the secret area say experience by doing binary explanation
and taking more time during the one than during the zero, sorry about the creative
the picture, but in some constant encode like that, the code is usually less readable
because we have to use different techniques and avoid certain patterns that we don't
want to have in our code.
It's usually a bit slower because we need to always take the maximum amount of time for
an operation and sadly also it's always a fight against the compiler because some of
the amazing compilers might recognize some constant time algorithms, some constant time construct
and decide to replace it by a faster and variable time construct.
So for instance, in the binary explanation, classical example, we transform the branch
depending on the on the bit of the exponent into a conditional select that is implemented
using masking and bitwise arithmetic and we must take care to transform our condition into
a mask properly in order to avoid some compiler optimizations and that's all well and good,
but it also leads to two code that is, as I said, less riddle and harder to understand,
and that's where I think Spark comes in because we can then prove the primitive that we use
to build our constant time algorithms in Spark with contracts.
So Spark brings, Spark brings obviously the assurance that we have no real time errors,
that we have already determination of algorithms and all that.
It also proves we can also be used to prove our bitwise operation, like the condition select or
the conditional swap and even though we cannot prove that these are effectively running in
constant time because of all the considerations about low level hardware things and
optimizations. We can prove that they effectively do what we want them to do, which is
select the values and swap the values as we want. And in fact, all constant input in essence
is if it's not written in pure assembly, it always relies on best default implementations.
We have to confiscate our intent from the compiler. We have to have the optimization barriers and
the best we can do to actually ensure that our code is constant time is to audit the assembly
output and measure the resources and use by our code when it's running.
Yeah. In the library, on top of having proofs for low level and bitwise operations,
I wanted to have some higher level proofs including a proof that it wrote for proving the addition
of two beginners. For that, I was quite surprised by the amounts of code that you need to
simple things in this part, but I think that's for most proofs in formal reasoning.
It takes always much more spark code and goes code than it takes actual logic to prove what we
want to prove. That proof is available on the GitHub repository, but it's not yet proved
all by the GitHub proof alia package. It's in a separate branch, but it works.
My main inspiration at first, because I was trying out Spark to write this library was to
try and write a small elliptic curve implementation, and so that's what I did in a small test.
Where I used the test vectors of the network to test my implementation. We can define
operations on a prime field by instantiating a generic package by defining the prime you want,
either at compile them or at runtime, and then instantiating the package you want.
And the first version of the library is available in the alia index right now.
And yet that's.
Any questions there?
And you say that actually constantly it's time code needs to be written assembly,
is there a choice of the alia or because I can imagine different compilers in the
different specific code, but also different CPUs doing interpreting differently,
or maybe micro to specialize in trying the history within the CPU?
Yeah, so how does a console name code really can be ensured to run?
Because even in assembly on different architectures and all that, it's kind of an open question,
because as I said in the slides, even a simple instruction like div can be running
in variable time depending on the appearance. There are no real solutions today,
I think, to that program, and it's mostly guessing and trying to do our best. But to actually
prove that some stuff is running in custom time, you will need a really deep integration with
the compiler and architecture, a language, and all that, and it's kind of an open question.
It's probably constant time, so some sort of why it was in the company that said in the end,
there should be a many compilers, and I think that would be a proper solution.
I'm like compilers like, or I don't know, like, in Seattle, maybe you can track them out of
something that could save this section of folks that use only constant time.
So the question is that the observation is that such a program should be solved at the compiler
level, mostly, and with specializations, specializations, annotations to say that such block
is in constant time and all that, and I can just say that.
I agree completely because, yeah.
Well, yeah, that's such a lot.
Where is what I want to do?
So that those constructs, and all that is kind, it's just manual branch,
it's just transforming the condition into a mask, and then
performing the two operations, and then just choosing the operation that we want.
It's a manual implementation of just doing branchless learning, in fact.
Yeah.
So in the concept primitive, I used a different time than Napoleon to explore the condition.
I chose to use in the concept.
I chose to use an opact type called choice that is in itself a mask.
So it's not a 0 or 1, it's a 0 or the maximum value of a U64.
And the reason is to kind of obfuscate what I want to do to the compiler, and also to avoid
doing some transformation all over the place, for instance, there are some operations that
already give me a mask, and I just want to be able to reuse it.
And so yeah, it just built another primitive to do that.
Yeah, you should try to get a conversation between the two, the variable time and the
time and the time and the issue.
Because once you see, we have, like, the need to teach you to see some missions that
have been done, but there will be a lot of different locations need to be done, so
time.
So there's a lot of research there, and perhaps we can now switch to something
like, you know, nothing which is rather nice.
And see whatever you can use in the XOI I was wondering, where it's, you can use that one
and it's pretty good, so I need to use it in the process, which is not a good way.
The question is whether the code is usable in performance critical environments.
And I would say that since the code is proven by Spark to be without front types of errors
and all that, it can be used without assertions and all that, so that kind of
consideration is really good. And there's always the fact that that we have to run
operations in the maximum amount of time in that bit. Yeah.
The library that I worry is not optimized for performance, there are some
operations that I don't implement in the best way, but in the the simplest way, sometimes.
So yeah, it could be used maybe with some development that you know.
There's not a lot of time left, so that may be one more question.
Maybe I don't think there should be that much difference between parallel and constant
code because I think that's a problem with this because if we have much entropy, then
I always have to know that I don't need to do that notification.
In like half the case and both, there's a lot of it and you will have to do the notification.
So I think that there's not much loss in the average case,
maybe half a pass or something, but what I want to ask is that if that's enough
I think that's enough.
Am I implementing a carousel by multiplication? No, not yet. It could be. I could do it,
but I haven't. In the original rest grade that I got heavily inspired from,
there is an implementation that decides at compile time whether to use carousel or
or classical multiplication, and I just copied the classical implementation of multiplication, because yeah.
During the implementation, how often did you have to actually look at the, there's a symbol of
the implementation that I have to look at often at the assembly output, and I did look quite
often at it because I wanted also to check whether my code was vectorized properly,
but the compiler under a lot. So I looked for, when building the parameters, I looked
quite often at the assembly output, and so yeah, it's maybe not a necessity always, but yeah.
So thank you.