Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Postdoc position at the University of Birmingham


view this post on Zulip Email Gateway (Nov 01 2022 at 15:08):

From: vincent rahli <vincent.rahli@gmail.com>
Dear all,

We would like to invite applications for an up to 3 years fully-funded
postdoctoral position within the School of Computer Science at the
University of Birmingham (see below for details on how to apply).

The successful candidate will contribute to an EPSRC-funded project aiming
at designing and formally verifying distributed systems, in particular
Byzantine fault-tolerant distributed systems as used for example in
blockchain technology.

The start date is flexible, ideally early 2023.

The environment:


The School of Computer Science has large and thriving Theory and Security
research groups. Among our research interests related to this project are
for example:

- Formal verification
- Proof assistants
- Model checking
- Blockchain Technology
- Security & Privacy

Both groups are very active, organising regular seminars, informal
meetings, and actively participating in many events such as the Midlands
Graduate School or the Cyber Security PhD Winter School. For more
information see
https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx
and
https://www.birmingham.ac.uk/research/centre-for-cyber-security-and-privacy/index.aspx
.

How to apply:


Interested people are encouraged to contact me by email (V.Rahli@bham.ac.uk)
to discuss their research interests and details of the positions. Further
information on how to apply is available here:
https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/521/?utm_medium=jobshare

Best,
Vincent Rahli

view this post on Zulip Email Gateway (Nov 01 2022 at 16:53):

From: Harry Butterworth <heb1001@gmail.com>
No doubt you’ve got something else in mind but…

If you write a layer of software to create a BFT implementation of the seL4
abstract specification on top of a cluster of seL4 nodes and then do a
refinement proof that your new layer implements the seL4 abstract spec,
assuming the constituent nodes also implement the abstract spec, then
you’ll create a useful bit of infrastructure that will be compatible with
the seL4 ecosystem.

Anything written to run on seL4 could be migrated to your platform to get
Byzantine fault tolerance with very little incremental programming effort.

You could size the project based on the published seL4 metrics and the
sizes of existing BFT platforms. It’s quite a lot of work to do everything
but it’s plausible to get an unverified BFT platform working with a few PY
of effort.

One advantage of this approach is that you’ll immediately start with an
existing formal spec of the API your project will need to implement so you
won’t waste time building the wrong thing.

There was an earlier seL4 replication project that might help. I was
looking out for it but have now lost track of whether or not it was ever
open sourced.

I expect there are multiple ways to implement the required software layer
but it would certainly be possible to use something blockchain-like in
there for the BFT distributed consensus required to manage the consistency
of the replicas.

I thought about doing this for fun a little while ago. One of the
difficulties was that the seL4 tool chain didn’t support concurrency. Some
kind of solution for that would be required for the refinement proof for
the distributed system: concurrency is inherent and must be modeled in
order to prove that it doesn’t cause a violation of the spec.


Last updated: Mar 29 2024 at 04:18 UTC