[Ur] Thoughts on cryptographic hashing for Ur/Web standard library?

[Matt Rice]

On Sat, May 19, 2018 at 12:52 PM, Adam Chlipala <adamc at csail.mit.edu> wrote:
> After a busy semester, I am going through the backlog of Ur/Web issue
> reports.  I'm hoping to make a new Ur/Web release soon, and here is the
> first in what may be a series of community queries, to decide whether
> certain changes are appropriate.
>
> It has been pointed out that Ur/Web's Basis.crypt uses DES, a weak hashing
> approach by today's standards.  I can think of a few potential courses of
> action:
>
> As in the linked PR, just add a comment essentially saying "hey, this crypto
> isn't so great."
> Switch to a different cryptosystem available in OpenSSL's libcrypto, which
> is already linked with all Ur/Web apps.
> Realize that literally no one is using this function and just delete it from
> the standard library.  (A less severe version is to ask a small but
> nonzero-size user community to switch to using separate libraries for this
> functionality.)
>
> Any thoughts?

Somewhat like 3 i imagine, but I'm not terribly enthusiastic about the
string -> string -> string type signature,
when we could implement so called "perfect crypto" modules in the type
system itself,
then implementers of this signature could back it with whichever
crypto primitives they like

There is quite a long correlation between ML's sealing/opaque
ascription as signatures for perfect crypto
e.g. see this paper from the ML workshop 2004,
http://www.cis.upenn.edu/~bcpierce/papers/infohide3.pdf
basically dating back the pre-ml days of
http://www.erights.org/history/morris73.pdf

relegating mechanism to a phantom type.

Since it is related, the basis function val rand : transaction int
Is another place I would desire a phantom type, e.g. val rand : rng ->
transaction (rng number)

In general though, I don't know enough about the compiler
implementation to know if adding these extra layers of abstraction
are going to impose runtime overhead, this way tends to add a lot of
type conversions/identity function calls,
which in theory could but may not be inlined across modules, in a way
that can be turned into a type cast.

but it does have the benefit of not needing to really anoint any one
primitive crypto mechanism.
*shrug* we can dream right?