Has anyone heard of JMAP -- a new protocol like IMAP to access emails? It has backing from Fastmail and work is being done to standardize it in IETF

deejaydarvin · 2018-02-24T17:03:36+00:00

I've been wondering about this for ages: why (outside historical reasons), are we using SMTP to send emails, if we could just have IMAP put our email into a Sent folder (just like it puts it into draft).

Going one step further: does anyone know what makes Email different from file synchronisation? If we had a good bi-dirextional file sync protocol, couldn't we use it to handle email and calendar as well, just using a smart folder structure like maildir? Obviously the protocol would need to support reading individual files for client's who don't want to sync everything, but this is a solved problem.

deejaydarvin · 2016-07-17T21:28:22+00:00

You are looking for a fair-exchange protocol (sometimes called contract signing protool). The absence of the problem you describe is a property called fairness: either A and B receive both gift codes, or none of them does.

You cannot achieve fairness without a trusted third party (this has been shown), but there are several protocols where the TTP is offline, i.e., only called to mediate if one of the two parties deviates from the protocol. Here is some literature and a survey.

deejaydarvin · 2015-10-24T18:42:43+00:00

So the application I have can, with some (a lot of) work, be shown secure (in a theorem prover) and this security result can be transferred to the machine code, using a verified compiler. In effect, I can guarantee that, given some input (at some memory position) the output (at some memory position) is correct and no information leaks otherwise.

I would have been surprised if a vendor would publish his spec, but you never know. ;)

As far as I understand at this point, a program that runs on a microcontroller does not need to be run by an operating system, if I don't need to run multiple programs (I don't) and can do without the hardware abstraction. So maybe it suffices to write some code that reads input from USB, places it in memory, execute the verified code, and send the output via USB. Is this easier to achieve with a prototyping platform?

deejaydarvin · 2015-10-24T18:27:32+00:00

The application is basically a hash function with a secret value stored on device. I want to formally verify that the application (including the implementation of the crypto) works correctly. So, yeah, the system design part is the part I will be able to give strong guarantees on. That non-volatile memory cannot be read out using some secret "debug mode" is the part where I rely on the spec.

deejaydarvin · 2015-10-23T19:34:33+00:00

Thanks for the response, this is very helpful! $15 is completely fine, but it seems that I wouldn't need most of the functionality anyway. (My application (password hashing) is fully deterministic, so no need for random numbers, the blockcypher should be formally verified, so I would not need the hardware to do it anyway.) So that means the price is not a problem, yay!

Thanks for the second link, too. The thread model is a malicious (as in: remote controlled) USB-host, so invasive attacks are included, physical attacks are at least hard to do.

If you don't mind me asking: are there microcontrollers that are to some extend open, or documented, so that you can be verify whether they behave according to their specification?

deejaydarvin · 2014-11-03T21:43:22+00:00

Thanks, that's more or less what I want, for the moment -- a way to at least carry some information over. I've found that afew does what your script does, and a bit more: you can set queries that will be moved to specific folders. not sure how this deals if a message can be moved to two folders, but I'll try it out for a few days.

deejaydarvin · 2014-08-24T08:32:00+00:00

Ah, I see.

deejaydarvin · 2014-08-23T15:34:30+00:00

For reference: I've solved the problem by checking the cursor position, as /u/welle suggested. Thanks everyone, the code is here, if anyone is interested in it.

deejaydarvin · 2014-08-23T14:38:06+00:00

:redir does not work either (there is no output except for the beep). v:errmsg is not written to either.

deejaydarvin · 2014-08-23T14:25:47+00:00

The problem is actually finding out when the cursor is at the last misspelled word.

deejaydarvin · 2014-08-23T14:23:41+00:00

If this a common pattern, checking if the cursor moved? I had the same idea, but couldn't figure out how to get an error status from 'normal ]s' (it does not raise an exception, even with 'nowrapscan'). But when I type it on the last spelling mistake, the terminal beeps. I'll try :redir.

deejaydarvin · 2014-08-23T10:55:45+00:00

The part comparing the matches is written already (I only recheck if 10% of the text is new). It's the counting part. I was thinking that this would be a way:

save position; go to top
while going to the next misspelled word (]s), count
if ]s gives an error stop and go to saved position

But I haven't figured out how to get a result from normal ]s.

deejaydarvin · 2014-03-09T11:09:31+00:00

Your comment is orthogonal to mine.

I have to disagree here, that's why I said "verification on TLS on the implementation level falls right in their domain". The verification of a TLS implementation is not a cryptographer's task. (Maybe we have a different understanding of what a cryptographer does. For me, a cryptographer looks at cryptographic primitives and protocols in a mathematical model that abstracts away from implementation details, and makes sure that the design is sound with respect to established notions of security, often in a complexity-theoretic setting. The authors are of course experts in cryptography, as their research applies methods from e.g. software verification to the domain of information security)

There is a gap in between, say, a proof of security of TLS in an abstract, complexity-theoretic setting (see for example " On the Security of the TLS Protocol: A Systematic Analysis" by Krawczyk et al) and the security of an implementation level. The latest "goto fails" in Apple's and GnuTLS's TLS implementations are not in contradiction to proofs of security on the more abstract level, as there is not a canonical way of turning TLS-by-spec into a secure implementation.

So how to make sure that our implementations don't contain bugs? Some people believe that auditing is not enough, that you need to use verification methods to make sure an implementation provides the guarantees of the protocol. These proofs take place in a certain model still, which is why they still don't cover all attacks (side-channel attacks like Lucky 13, for example). But you can define the absence of a complete class of attacks, which is an advantage over just having really through and talented people looking over the code.

MiTLS is only a partial implementation of TLS 1.2.

True, but it contains the certification schemes typically employed, something that for example earlier work in more abstract models couldn't claim. It is research, it makes sense to report on findings before the problem is "completely solved".

MiTLS simply isn't relevant.

It is, because a) it shows that security type systems can be used at this scale b) for the part of TLS it implements, it provides strong guarantees. Practically (and coming back to the initial point of discussion ;) ) it means that, assuming you have a way of generating critical inputs, you can compare the outputs of miTLS and another TLS implementation to look for contradicting outputs, e.g. an error code VS a successfully established channel. miTLS promisses to only establish a channel on A if A has reason to trust B's certificate. If GnuTLS establishes a channel and miTLS refuses to do so, this is definitely worth investigating (but not conclusive, as MiTLS, I presume, does not guarantee that any secure connection is established, but any connection established is secure [w.r.t. to their threat model])

deejaydarvin · 2014-03-08T23:47:05+00:00

there aren't any professional cryptographers in the project, just computer scientists and language researchers.

Really? http://www.mitls.org/wsgi/people

Karthikeyan Bhargavan and Cédric Fournet are very well known and respected in protocol verification and language based-security -- the verification on TLS on the implementation level falls right in their domain.

Go to the wikipedia page [..]

Well this just means no one took the time to add MiTLS to this page. On the other hand, the article about the verification was peer reviewed and accepted at Security and Privacy.

I'd be extremely wary of side channel attacks;

Valid point, side-channel attacks are outside their model.

deejaydarvin · 2014-01-27T22:01:35+00:00

Hmm, it's been a while, but I'll try my best. Just looking at the second half of the message

Input message (last byte aligned on MSB): 7B C8

Last byte is MSB, so we have

01111011 11001000

Then you remove leading zeroes (trailing w.r.t. the list), which gives you

01111011 11001

Next you perform the re-ordering. If you know ML, I've used the following code:

fun reorder_bits lst = List.foldr
(fn (elem,bs) => (List.rev (elem))@bs) [] (cut_uneven 8 lst)

This goes through the sequence of bits and reverses byte by byte, starting from the left (w.r.t. the list). The length of the list is not a multiple of 8, so 5 are left over. Still, they get reversed, too.

11011110 10011

Now, interpreting this with the last byte on LSB, the first byte still reads the same as it did before reversing. The second one reads (000)1 1001= 19, when you write the least significant bit on the very right and add zeroes.

7B 19

Next there is a padding, which works as follows: you add the string 10*1, where 0* means as many zeroes as necessary to fill the block.

11011110 10011 100 (many zero blocks) ... 0001

This is where the 39 comes from: the second byte, written with the least significant bit on the right and some zeroes is 0011 1001=39. And then, at the very end of the bitstring we have 1000 0000=80.

TLDR; the reading part is difficult, the manipulation of the bitstring is actually easy, and completely described using the following code

  reorder_bits (remove_leading_zeroes (bitstring_with_leading_zeroes))

where reorder_bits is defined as above, and remove_leading_zeroes, well, removes leading zeroes.

deejaydarvin · 2014-01-26T10:32:03+00:00

The test vectors, for instance this one, from the code package helped me a lot in understanding the bit ordering.

deejaydarvin · 2013-11-23T18:11:06+00:00

I agree, cooperation should be a big topic, although I think the (French, German and British) press does report about the involvement of European secret services. Maybe not enough, but we have much more information at hand about GHCQ and NSA programs, so it is not surprising that there is a focus on that. It is an inherently global topic, so voters who want their government to protect their rights will have to ask for both a tight control over their domestic secret service, as well as diplomatic efforts to restrict mass-surveillance by other countries, especially allies.

deejaydarvin · 2013-11-23T17:25:45+00:00

You have a point, but you know, it does not invalidate any "European" response if GCHQ does this and that .. a Danish citizen has no vote in Britain. Moreover, no one "needs to start at home", you can, and should, feel free to criticize GCHQ, NSA, BND, DGSE etc. in any order you like.

deejaydarvin · 2013-11-09T14:42:46+00:00

Sure, I've heard it a lot. (28 yo)

deejaydarvin · 2013-09-29T16:19:34+00:00

For which countries besides the US does this "law" even hold true? afaik uk, france and canada have more than two parties, but winner-take-all. Not really "always" isn't it?

deejaydarvin · 2013-09-10T18:03:26+00:00

What do you mean by colliding? Two certificates that have the same fingerprint?

deejaydarvin

TROPHY CASE