Re: [Ur] need help with unification and field name disjointness proof failures
On 04/08/2017 04:05 PM, Adam Chlipala wrote: On 04/06/2017 06:22 PM, Benjamin Barenblat wrote: The fact that `rand` returns -1 on failure, however, is a bit scary. That sounds like a CVE waiting to happen – people aren’t going to check the result code from `rand`. Adam, how would you feel about it returning an `option` or throwing an application error if it fails? Raising an error seems like a reasonable idea. It could signal to snooping parties that we ran out of entropy, but I hope that isn't such a serious leak. Any other strong opinions from people watching the list? OK, absent other opinions, I implemented raising an error. ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
On 04/06/2017 06:22 PM, Benjamin Barenblat wrote: The fact that `rand` returns -1 on failure, however, is a bit scary. That sounds like a CVE waiting to happen – people aren’t going to check the result code from `rand`. Adam, how would you feel about it returning an `option` or throwing an application error if it fails? Raising an error seems like a reasonable idea. It could signal to snooping parties that we ran out of entropy, but I hope that isn't such a serious leak. Any other strong opinions from people watching the list? BTW, Ur/Web is also already using cryptographic hashing internally, for CSRF cookie signatures, so perhaps it also makes sense to expose functionality of your other library by default. ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
On Thu, 06 Apr 2017 17:25:53 -0400, Adam Chlipala wrote: > > On 04/06/2017 04:52 PM, Benjamin Barenblat wrote: > > In addition, on your first TODO (‘use better crypto functions’), you > > may be interested in my cryptographic random¹ and hash² libraries. I’d > > be thrilled to incorporate patches for the latter if you want to add > > more OpenSSL hash functions (PBKDF2 in particular would be extremely > > welcome and probably quite applicable to your current work). > > > > ¹ https://benjamin.barenblat.name/git/urweb-crypto-random-openssl.git > > ² https://benjamin.barenblat.name/git/urweb-crypto-hash-openssl.git > > I thought Ur/Web's built-in [rand] function was already cryptographically > secure. Did I > get something wrong there? It's the crypt function that I'm concerned about. pgphqtFjrHt1Z.pgp Description: OpenPGP Digital Signature ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
On Thu, 06 Apr 2017 16:53:50 -0400, Benjamin Barenblat wrote: > > Er, excuse me. s/database/table/g. You can use `oneOrNoRows` to query > multiple *tables* simultaneously. Thanks a lot for the helpful explanation! Much appreciated. Lesson learned: read the type signatures more thoroughly! Marko pgp1xQXxEbTKx.pgp Description: OpenPGP Digital Signature ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
*looks at Ur/Web source* It is! I wonder why I wrote urweb-crypto-random-openssl. My best guess is that I was concerned by the fact that `rand` returns -1 on failure instead of throwing an application error. On the other hand, freaking out and writing my own library seems a bit of an overreaction. More likely I just didn’t bother to check the randomness properties of the built-in `rand` and assumed that it wrapped C `rand`. The fact that `rand` returns -1 on failure, however, is a bit scary. That sounds like a CVE waiting to happen – people aren’t going to check the result code from `rand`. Adam, how would you feel about it returning an `option` or throwing an application error if it fails? ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
On 04/06/2017 04:52 PM, Benjamin Barenblat wrote: In addition, on your first TODO (‘use better crypto functions’), you may be interested in my cryptographic random¹ and hash² libraries. I’d be thrilled to incorporate patches for the latter if you want to add more OpenSSL hash functions (PBKDF2 in particular would be extremely welcome and probably quite applicable to your current work). ¹ https://benjamin.barenblat.name/git/urweb-crypto-random-openssl.git ² https://benjamin.barenblat.name/git/urweb-crypto-hash-openssl.git I thought Ur/Web's built-in [rand] function was already cryptographically secure. Did I get something wrong there? ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
Er, excuse me. s/database/table/g. You can use `oneOrNoRows` to query multiple *tables* simultaneously. ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] need help with unification and field name disjointness proof failures
Your code assumes `oneOrNoRows` returns an `option {Username : string,
PasswordHash : string, Salt : option string}`. In actuality, you can
use `oneOrNoRows` to query multiple databases simultaneously, so it
puts results from each database into a record field. In this
particular example, it returns `option {User : {Username : string,
PasswordHash : string, Salt : option string}}` (because `User` is the
name of the database that you’re querying, transformed to be a field
name). If you are just querying one database, consider using
`oneOrNoRows1`, which returns the type that you want.
In addition, on your first TODO (‘use better crypto functions’), you
may be interested in my cryptographic random¹ and hash² libraries. I’d
be thrilled to incorporate patches for the latter if you want to add
more OpenSSL hash functions (PBKDF2 in particular would be extremely
welcome and probably quite applicable to your current work).
¹ https://benjamin.barenblat.name/git/urweb-crypto-random-openssl.git
² https://benjamin.barenblat.name/git/urweb-crypto-hash-openssl.git
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
[Ur] need help with unification and field name disjointness proof failures
The attached source is giving me some type related errors. I'd very
much appreciate some help ...
Thanks,
Marko
password.ur
Description: Binary data
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:56:4: (to 67:0)
Error in final record unification
Can't unify record constructors
Have:
++ [Salt = option string, PasswordHash = string]
Need:
[User =
{Salt : option string, PasswordHash : string, Username : string}]
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:56:4: (to 67:0)
Stuck unifying these records after canceling matching pieces:
Have:
([Salt = option string, PasswordHash = string]) ++
Need:
[User =
$((fn fields :: ({Type} * {Type}) => fields.1)
(([Salt = option string]) ++
([PasswordHash = string]) ++ [Username = string], []))]
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:55:0: (to 67:0) Some
constructor unification variables are undetermined in declaration
(look for them as "")
Decl:
.
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]]) ++
([]) ++ []] [[]] [[]] [string] [string] [bool]
(Basis.sql_eq [string])
(Basis.sql_field [([]) ++ []]
[([]) ++ [Salt = option string, PasswordHash = string]]
[string] [[]] [[]] [#User] [#Username])
(Basis.sql_inject
[([User =
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]])
++ ([]) ++ []] [[]] [[]] [string]
Basis.sql_prim [string] Basis.sql_string r.#User),
GroupBy =
Basis.sql_subset_all
[[User =
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]]],
Having =
Basis.sql_inject
[([]) ++
[User =
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]]]
[([]) ++
[User =
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]]]
[[]] [bool] Basis.sql_prim [bool] Basis.sql_bool Basis.True,
SelectFields =
Basis.sql_subset
[[User =
(([Salt = option string]) ++
([PasswordHash = string]) ++ [Username = string], [])]],
SelectExps = {}},
OrderBy =
Basis.sql_order_by_Nil
[([]) ++
[User =
([Username = string]) ++
([]) ++ [Salt = option string, PasswordHash = string]]] [[]],
Limit = Basis.sql_no_limit, Offset = Basis.sql_no_offset}))
(fn thisUser :
option
$(([Salt = option string]) ++
([PasswordHash = string]) ++ ) =>
case thisUser of
None =>
return [transaction] [option string] Basis.transaction_monad
(None [string]) |
Some u =>
case u.#Salt of
None =>
return [transaction] [option string] Basis.transaction_monad
(None [string]) |
Some s =>
case
Basis.eq [string] Basis.eq_string u.#PasswordHash
(crypt r.#Pass s) of
Basis.True =>
return [transaction] [option string] Basis.transaction_monad
(Some [string] r.#User) |
Basis.False =>
return [transaction] [option string] Basis.transaction_monad
(None [string]))
.
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:63:15: (to 63:29)
Couldn't prove field name disjointness
Con 1: [PasswordHash = string]
Con 2: ([Salt = option string]) ++
Hnormed 1: [PasswordHash = string]
Hnormed 2: ([Salt = option string]) ++
/home/marko/myStuff/Projects/AssignTAs/sandbox/password.ur:60:13: (to 60:19)
Couldn't prove field name disjointness
Con 1: [Salt = option string]
Con 2: ([PasswordHash = string]) ++
Hnormed 1: [Salt = option string]
Hnormed 2: ([PasswordHash = string]) ++
pgpb2KEC0eGOk.pgp
Description: OpenPGP Digital Signature
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
