avsm changed the topic of #mirage to: mirage 2 released! party on!
nordwp_home has joined #mirage
haesbaert has joined #mirage
nordwp_home has quit [Ping timeout: 240 seconds]
nullcat has joined #mirage
nordwp_home has joined #mirage
lobo has quit [Quit: leaving]
nullcat has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
nullcat has joined #mirage
nullcat has quit [Read error: Connection reset by peer]
nullcat has joined #mirage
yegods has quit [Remote host closed the connection]
mort___ has joined #mirage
mort___ has left #mirage [#mirage]
nullcat has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
pyvpx_ has joined #mirage
oskarth_ has joined #mirage
NhanH_ has joined #mirage
smkz_ has joined #mirage
smkz_ has quit [Changing host]
smkz_ has joined #mirage
Drup has quit [Ping timeout: 240 seconds]
oskarth has quit [Ping timeout: 240 seconds]
NhanH has quit [Ping timeout: 240 seconds]
smkz has quit [Read error: Connection reset by peer]
pyvpx has quit [Ping timeout: 240 seconds]
Drup has joined #mirage
NhanH_ is now known as NhanH
oskarth_ is now known as oskarth
Druup has joined #mirage
Drup has quit [Ping timeout: 240 seconds]
pyvpx_ is now known as pyvpx
lobo has joined #mirage
yegods has joined #mirage
lobo has quit [Quit: leaving]
lobo has joined #mirage
Druup is now known as Drup
yegods has quit [Remote host closed the connection]
_whitelogger has joined #mirage
reynir has quit [Disconnected by services]
reynir1 is now known as reynir
seako_ has joined #mirage
oskarth_ has joined #mirage
dobson` has joined #mirage
sigjuice_ has joined #mirage
oskarth has quit [*.net *.split]
seako has quit [*.net *.split]
sigjuice has quit [*.net *.split]
_whitelogger_ has quit [*.net *.split]
dobson has quit [*.net *.split]
seako_ is now known as seako
oskarth_ is now known as oskarth
lobo has quit [Quit: leaving]
<maker>
ohai. is there any link available where I can check out the work done on some components of mirageos involving formal methods?
<maker>
I would be super-interested in knowing if anybody has ever produced a formal proof of the security of component X in mirage.
nullcat has joined #mirage
<maker>
:(
<mattg>
hi maker, the IRC channel isn't super-active, but if you sent an email to mirageos-devel@lists.xenproject.org I' sure you'd get some interesting answers
<mattg>
sorry I can't help you directly with your question !
<maker>
mattg: oh, okay. Thanks!
<maker>
This is actually a question a asked to noddy2OOO a couple of years ago. I just have more free time (and a bit skills) now.
<Drup>
maker: afaik, nobody did any work to formaly verify any *implementation*
copumpkin has joined #mirage
<maker>
Drup: uhm. I'm not even sure there are the tools for this. It shouldn't be impossible though in an easy adversarial model like dolev-yao
<Drup>
for formaly verrifying ocaml implementations ? coq ...
<maker>
Drup: yes, coq is fine, but you have to make explicit all reductions an adversary can do, and verify some properties on the closure of this reductions
<Drup>
(disclaimer: I'm not doing anything remotely related to security)
<maker>
(disclaimer: I don't know shit, really)
<maker>
:)
<maker>
haha, apparenlty proverif is even mono-process
raindev has joined #mirage
nullcat has quit [Read error: Connection reset by peer]
nullcat has joined #mirage
raindev has quit [Ping timeout: 240 seconds]
raindev has joined #mirage
raindev has quit [Remote host closed the connection]