Julia Community 🟣: Jānis Erdmanis

Introducing PeaceFounder

Jānis Erdmanis — Tue, 19 Sep 2023 23:17:20 +0000

Around four years ago, I began exploring electronic voting (e-voting) systems by scratching an itch I had. The journey, although challenging, has been enlightening, and I have been focusing on the development of a new e-voting system since I graduated from my PhD program two years ago. Today, I am excited to introduce you to the PeaceFounder project, which is not just another e-voting system but one that aims to raise the bar and overcome the limitations of mainstream E2E verifiable voting systems.

PeaceFounder is built upon the idea of verifiably anonymising voters' pseudonyms rather than their votes. This addresses the tension between security, transparency and privacy without requiring the coordination and meticulous risk assessments of threshold decryption ceremonies. This is achieved by the transactional nature of the anonymisation procedure called braiding, which shuffles and exponentiates all pseudonyms with a secret factor and provides zero-knowledge proof for doing that honestly, much like tying a knot, as shown in the picture.

These proofs are published on the bulletin board for everyone to audit. The PeaceFounder bulletin board is inspired by developments in the auditability of certification authority with history trees, where the goal is to prevent a malicious authority from silently issuing a spoofing certificate, giving a backdoor where it can get your passwords and tokens in plaintext. History tree allows hosting the bulletin board on a single server while member devices keep it accountable to the immutability of records with consistency proofs without needing to do a full replication. This is used for votes, membership certificates, proposals, and braids and, in so, establishes a public transactional log which can be run as a state machine.

Both of these innovations enable a single individual to set up the system, register members, braid pseudonyms, announce proposals and collect votes while neither compromising security, transparency or privacy. On top of that, pseudonymity enables the formation of arbitrary complex ballots, which are no longer limited to human counting workloads. The pseudonymity also enables fluid voting where voters can change their vote at predetermined times, bridging the gap between representative and direct democracy. Also, it is possible to shard a long ballot into smaller sections distributed between voters so that voters have less decision fatigue and are empowered with larger responsibility, resolving the longstanding paradox of voting. Thinking about it keeps me damn excited.

On the technical programming side, PeaceFounder demonstrates Julia's remarkable potential by showcasing its power in full-stack applications, affirming that Julia's capabilities are a reality. Crafting a bridge between Julia and QML was challenging, but I ultimately succeeded when I understood the model-view-controller paradigm. I didn't have to touch a single C++ file or compile anything since QML.jl and Yggdrasil provided everything out of the box.

I adopted a test-driven development approach, which involved drafting an API for components to synergise before diving into Julia for implementation. I made a conscious effort to avoid brittle wrappers, leading to the reimplementation of the Verificatum-compatible proof of shuffle, which was initially only available in Java. Additionally, I chose to implement cryptographic groups and signatures in Julia instead of using C library wrappers.

Throughout the project, I prioritised purity and simplicity. Packages like CryptoSignatures, ShuffleProofs, and HistoryTrees embody these principles with a narrow API that lifts mountains behind them. However, this rule was broken with CryptoGroups, which could be scrambled in many tiny packages and thus, writing documentation for it is a chore. This reminds me of a mistake I made early on in the project by registering many small packages like SecureIO, BraidChains, DemeNet, Synchronizers, Multiplexers, and DiffieHellman. As a result, only 30% of packages have evolved and survived. Nonetheless, I plan to revive some of these in the future, ending with about 50% survivals and improving this rather ugly situation.

Currently, a demo of PeaceFounder is available without voiceover commentary that allows for a quick grasp of the project's essence and preliminary status. The upcoming milestones include the development of an administrative panel and a seamless user interface that eliminates the need for terminal interactions.

As with any endeavour of such magnitude, challenges abound. Over recent months, I have been invested in clarifying the project's purpose and edge over competitors and articulating design intricacies, now available at peacefounder.org. This was a good time to take a step back from development to get back in with revived vigour. With essential documentation in place, the PeaceFounder project has reached a milestone where the Julia community can make a difference. Your feedback, scrutiny, and potential coding improvements are welcomed. Specific areas of code contribution are outlined on peacefounder.org/roadmap.

I recognise that Julia emphasises high-performance tasks, which drove my decision to exclusively use it for numerical computations, leveraging the powerful DifferentialEquations and QuantumOptics during my PhD. While developing the PeaceFounder project, I never felt inclined to switch to languages like Python, C, C++, or Rust. The interactive development facilitated by tools like Revise and Infiltrator expedited the creation of the demo.

Looking ahead, the static compilation issue is a dealbreaker since I wish to deploy the client to mobile. Currently, it seems I will need to port the client backend in Rust, which could interface with an already written QML facade and offer Arti a TOR client library necessary to prevent traceability. Nevertheless, I don't look at my decision to do the project in Julia as a mistake, as it enabled me to iterate quickly and put the ideas into a form with a Julia's type system. It also puts me on a frontier for writing high-performance cryptography where, for instance, proof of shuffle (see ShuffleProofs) is a highly parallelisable algorithm which can benefit from being run on an HPC cluster for a large-scale application.

In addition, I have faced some other gripes, such as the hurdle of direct module importing without erasing global variables. This makes me hesitant to adopt Oxygen within a module, as a hack is needed, as highlighted in this issue. Another difficulty I face is documenting highly overloaded methods where I wish the code could be stricter, perhaps with something like a trait/interface. The dynamics around type parameter values and the need to bypass the isbitstype requirement have also been limiting. Using Mods as an example, type parameters conveniently store the modulus, allowing for compact vector representation, but fails with BigInt. I use this extensively in ShuffleProofs.jl, which gets me to write pseudocode while allowing me to raise errors at the dispatch stage when groups are not aligned.

In conclusion, PeaceFounder embodies years of dedication, research, and personal growth. I would greatly appreciate to receive feedback, scrutiny, and potential coding improvements. A GitHub star on PeaceFounder.jl would also not hurt :) On the horizon, I'm gearing up to present a poster at the EVoteID conference in Luxembourg. Also, as my personal resources start to run dry, I'm actively seeking financial support and would appreciate anyone who could mentor me through this.

A DSL for choreographic programming in Julia?

Jānis Erdmanis — Tue, 20 Sep 2022 15:01:51 +0000

About a week ago, while looking into papers, I diagonally stumbled into a concept of choreographic programming. The idea is that instead of writing a separate program for each endpoint, we could simultaneously write a single program for all participants in a simple Alice and Bob notation, as one can find in protocol descriptions on Wikipedia. The hard part, though, is designing reasonably clear primitives while being able to project them to endpoints correctly, and this is what the vast research on choreographic programming is about.

The most minimal taste of choreographic programming is describing the types/labels of messages which travel between participants while leaving the implementation of the endpoints to a programmer. The benefit of doing so is that implementers of the protocol are free to choose their language and use the global specification to test that it is correct, just like typing does in statically typed programming languages. It is, in fact, called multiparty session types, where session refers to communication which takes place.

A recent example gaining popularity in this direction is Scribble. A typical code for it is shown below:

global protocol BookJourney (role Customer as C, role Agency as A, role Service as S) {
    rec LOOP {
    choice at C {
        query (journey: String) from C to A;
            price (Int) from A to C:
            info (String) from A to S;
            continue LOOP;
        } or {
            choice at C {
            ACCEPT() from C to A;
            ACCEPT() from A to S;
            Address(String) from C to S;
            (Date) from S to C;
        } or {
            REJECT() from C to A;
            REJECT() from A to S;
}  }  }  }

Chor takes another approach. In addition to defining communication types, it also allows for writing the protocol in one block for all endpoints at the same time:

program customer_agency;

protocol PurchaseProtocol {
  Customer -> Agency: CheckPrice
  askPrice(string);
}

protocol CheckPrice { 
  Agency -> Customer: price(int);
  Customer -> Agency: {
    askPrice(string);
    CheckPrice, 
  accept(void);
    Customer -> Agency: order(string);
    Agency -> Customer: date(string), 
  reject(void)
  }
}

public agency_url: PurchaseProtocol

define checkPrice(c,a)(s[CheckPrice:c[Customer], a[Agency]]) {
  ask@a(prod,price);
  a.price -> c.price: price(s); 
  ask@c(price,satisfied); 
  if(satisfied == "Yes")@c {
    ask@c("Confirm?",confirm); 
    if (confirm == "Yes")@c {
    c -> a: accept(s);


    c.prod -> a.prod: order(s); 
    ask@a(prod,date);
    a.date -> c.date: date(s)
    } else {
    c-> a: reject(s)
    } 
  } else {
    ask@c("Product Name",prod); 
    c.prod -> a.prod: askPrice(s); 
    checkPrice(c,a)(s)
   } 
 }

 main {
   c[Customer] start a[Agency]: agency_url(s);
  ask@c("Product Name",prod);
  c.prod -> a.prod: askPrice(s); 
  checkPrice(c,a)(s)
}

Notice the @; it is a way of telling that the function is executed on a particular endpoint. Although It is a bit ugly that new variables are created within the functions.

A Pirouette uses an alternative approach, where a multiparty session type is constructed from the program itself.

Buyer.book_title ⇝ Seller.b; 
Seller.prices[b] ⇝ Buyer.p; 
if Buyer.(b < budget)
    then Buyer[L] ⇝ Seller;
    Seller.get_delivery_date(b) ⇝ Buyer.d_date;
    Buyer.(Some d_date) 
else 
    Buyer[R] ⇝ Seller;
    Buyer.None

And it also attempts to describe what functions of a global protocol could look like. Unfortunately, currently, this language does not seem to be implemented.

Academically choreographic programming language can be used as an approachable alternative to describing a protocol to prove its security properties. The best one that struck me in investigating the choreographic programming landscape is available in the paper "Security Protocols as Choreographies":

Alice → TPM: Boot 
TPM:pcr:=’1’ 
TPM → Alice: Booted 
Alice: new n, new esk 
Alice → TPM: Session , tpmk , aenc(esk , tpmk) 
TPM: new sid 
TPM → Alice:sid 
Alice → TPM:senc((Extend , n, sid), esk) 
TPM: pcr := hash(n, pcr) 
TPM → Alice: Extended 
Alice → TPM: Create , hash(’obt ’, pcr) 
TPM:newk 
TPM → Alice:sign((Created ,k,hash(’obt ’, pcr)), inv(tpmk) ) 
Alice:new v 
Alice → Parent: Envelope , enc(v, k) 
Parent: new esk 
Parent → TPM: Session , aenc(esk, tpmk) 
TPM: new sid
TPM → Parent:sid 
Parent → TPM:{ 
    senc((Extend ,’ref ’, sid), esk): 
    TPM: pcr := hash(’ref ’, pcr) 
    TPM → Parent: Extended 
    Parent → TPM: Quote ,enc(v,k) 
    TPM → Parent:sign((Quoted ,pcr,enc(v,k)),inv(tpmk)) 
    event secret(v) 
+
    senc((Extend ,’obt ’, sid), esk): 
    TPM: pcr := hash(’obt ’, pcr) 
    TPM → Parent: Extended 
    Parent → TPM: Decrypt , enc(v, k), sign((Created , k, pcr), inv ( tpmk ))
    TPM → Parent:v 
}

Apart from the fact that it does not use variables, it is a language I would love to program distributed systems.

Imagining a choreographic DSL in Julia

The most attractive approach, in my opinion, is taken by Piriotette. However, branching does feel a bit sloppy, where the programmer is expected to inform relevant endpoints on which branch is taken after the branch is taken. Also, the dot syntax is so OOP and ; is perhaps unnecessary, as we can see in the previous code example. Let's see if that can be made syntactically better.

The sending of messages could follow a simple Alice and Bob notation using a column as it is often done and presume that variable names at endpoints do have the same name and provide the as keyword to set it different at the endpoint.

Buyer -> Seller: book_title
Seller -> Buyer: prices[book_title] as p

So that was simple. Let's now jump into branching. It would be great that the branching part of the code would not involve informing involved parties on which branch has been taken. This is why I find this syntax most appropriate:

Buyer: choice = price < budget ? Left : Right
select Buyer -> Seller [choice]
case Left:
     # WHAT TO DO IN THIS BRANCH
case Right:
     # WHAT TO DO IN THIS BRANCH
end

Which follows the TPM example and replaces {} with case <label>:, adds a select keyword for signifying what it is. A bracket is added for informing how choice is calculated [<choice>] and follows the academic convention as a->b[l] is used to denote a label in process calculus (read it somewhere).

The last thing we must consider is how this protocol shall be packaged and used. Each agent can have its own set of inputs in the protocol. That we can address by having a function signature like:

function BookSeller((book_title, budget)@Buyer, (get_delivery_date)@Seller)

    ...

    Buyer: return "Finished."
    Seller: return "Done."
end

Note that the use of @ may not sit well within Julia, which uses it for calling macros. Any other symbol may suffice there.

The primary motivation for writing the protocol in a single function is that we want to test that it works. In contrast to the usual situation where one needs to call the code concurrently at the endpoints and deal with errors being hidden in those threads, an alternative way could be simply running it run globally:

book_title = "Iliad"
budget = 100
get_deliver_date(x) = 2050

result = BookSeller((book_title, budget)@Buyer, (get_delivery_date)@Seller)

@test result@Buyer == "Finished."
@test result@Seller == "Done."

We take the BookSeller protocol and project it with corresponding endpoints to run the protocol at the endpoints.

io = Link()

t1 = @async begin
    book_title = "Iliad"
    budget = 100
    BookSeller@Buyer(book_tile, budget; Seller=io)
end

t2 = @async begin
    get_deliver_date() = 2050
    BookSeller@Seller(get_delivery_date; Buyer=io)
end

@test result(t1) == "Finished."
@test result(t2) == "Done."

To implement Link, only send and recv functions need to be supplemented:

send(x::Int, io::Link) = raw_send(string(x), io)
recv(::Type{Int}, io::Link) = parse(Int, raw_recv(io))

This way, we can reuse the same protocol with different serialisation formats of choice, let it be either "JSON", "TOML", or even "ASN.1".

To assist in implementing a data marshalling channel, it would be helpful to infer the types of messages used for communication and test the link implementation accordingly. At the high level, it could look something like:

message_types = infer_message_types(BookSeller, ((String, Int)@Buyer, (typeof(get_delivery_date)@Seller))

@test isspecified(Link, message_types)

The isspecified method would then go through each message type and check that the corresponding method for marshalling and unmarshalling is implemented. In addition, if the type implements a sample method returning some random value for a given type, it could also check statistically that unmarshal(marshal(x))==x.

Lastly, a monitor could be fired up at the endpoint. That way, it could be detected if a remote party deviates from the protocol. However, this would require every message to have a unique distinct label for unmarshaling without input from the protocol.

Lastly, to finish this speculative specification, let's discuss modularity. Functions are integral to any large-scale program, allowing us to test things in pieces and assemble complex protocols. Taking inspiration from Pirouette, I arrive at the following idea:

function BookSeller(F, (book_title, budget)@Buyer, (get_delivery_date)@Seller)
    Buyer -> Seller: book_title
    Buyer: decision = F((prices[b])@Seller, (budget)@Buyer))
    select Buyer -> Seller [decission] 
    case Left:
        Seller -> Buyer: get_delivery_date(book_title) as d_date; # We expect no output from the Seller
        Buyer: return d_date
    case Right:
        Buyer: return nothing
    end 
end

The function then could be as simple as:

function F((p)@Seller, (budget)@Buyer)
    Seller -> Buyer: p
    Buyer: return p < budget
end

To pass it to the BookSeller, we could do something as simple as:

result = BookSeller(F, (book_title, budget)@Buyer, (get_delivery_date)@Seller)

Similarly, we could proceed at the endpoint.

A difficulty arises when we want to introduce another agent within the protocol. Consider another implementation of F:

function F((p)@Seller, (budget)@Buyer, ()Buyer2)
    Seller -> Buyer, Buyer2: p
    Buyer2 -> Buyer: p/2 as contrib
    Buyer: return (p - contrib) < budget
end

To test it, we could proceed using a closure:

G((p)@Seller, (budget)@Buyer) = F((p)@Seller, (budget)@Buyer, ()@Buyer2)
result = BookSeller(G, (book_title, budget)@Buyer, (get_delivery_date)@Seller)

A bit ugly part is that G needs to be provided with a link for Buyer2 explicitly, which needs to be done with closure or redefinition of the protocol:

BookSellerExtended((p)@Seller, (budget)@Buyer, ()@Buyer2) = BookSeller(
    ((p)@Seller, (budget)@Buyer) -> F((p)@Seller, (budget)@Buyer, ()@Buyer2),
    (book_title, budget)@Buyer, (get_delivery_date)@Seller
)

Whether it is defined here or at the endpoint is a matter of taste. In some situations where a complete F is unavailable, it could be implemented at the endpoint and placed in a place of F though that no longer could provide guiding rails to assist correct implementation.

It was fun to think about this problem, but it seems like an overwhelming project to take on. The main question remains whether it would be usable in practice and whether, if such DSL existed for what kind of problems it would be best suited for. Dining philosophers do not seem to be one of them, whereas a symmetric block cypher seems plausible if recursion or jumps are used at select statements.

Anyway, my itch with investigating and writing this post is scratched. I hope you enjoy thinking about choreographic programming, what it could enable you to do, and its pitfalls.

References

Bruni, A., Carbone, M., Giustolisi, R., Mödersheim, S., Schürmann, C. Security Protocols as Choreographies. (2021)
S. Giallorenzo, F. Montesi, M. Peressotti, D. Richter, G. Salvaneschi, and P. Weisenburger, Multiparty Languages: The Choreographic and Multitier Cases. (2021)
D. Ancona et al., Behavioral Types in Programming Languages, FNT in Programming Languages. (2016)
Andrew K. Hirsch and Deepak Garg. Pirouette: Higher-Order Typed Functional Choreographies https://www.youtube.com/watch?v=ES1bhxcRDy0 (2022)
Cover image: https://pxhere.com/en/photo/1606406