{"action":"created","issue":{"url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/162","repository_url":"https://api.github.com/repos/dhall-lang/dhall-haskell","labels_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/162/labels{/name}","comments_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/162/comments","events_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/162/events","html_url":"https://github.com/dhall-lang/dhall-haskell/issues/162","id":265320028,"number":162,"title":"Discuss safety options for Dhall","user":{"login":"Gabriel439","id":1313787,"avatar_url":"https://avatars3.githubusercontent.com/u/1313787?v=4","gravatar_id":"","url":"https://api.github.com/users/Gabriel439","html_url":"https://github.com/Gabriel439","followers_url":"https://api.github.com/users/Gabriel439/followers","following_url":"https://api.github.com/users/Gabriel439/following{/other_user}","gists_url":"https://api.github.com/users/Gabriel439/gists{/gist_id}","starred_url":"https://api.github.com/users/Gabriel439/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gabriel439/subscriptions","organizations_url":"https://api.github.com/users/Gabriel439/orgs","repos_url":"https://api.github.com/users/Gabriel439/repos","events_url":"https://api.github.com/users/Gabriel439/events{/privacy}","received_events_url":"https://api.github.com/users/Gabriel439/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2017-10-13T15:01:02Z","updated_at":"2017-12-16T18:34:02Z","closed_at":null,"author_association":"COLLABORATOR","body":"The purpose of this issue is to discuss what the command-line API for the `dhall/dhall-*` executables should be when users want to disable certain Dhall features for additional safety\r\n\r\nThe most common requests I've gotten for how to improve safety are:\r\n\r\n* Import-related safety:\r\n    * **Option 1**: Disable all imports except `ipfs` imports\r\n        * Disable all URLs except `https://ipfs.io/*`\r\n        * Disable all paths except `/ipfs/*` (for use in conjunction with `ipfs mount`)\r\n        * Disable all environment variable imports\r\n        * This permits ease of distribution of Dhall libraries (like the Prelude)\r\n        * This makes Dhall expressions mostly pure\r\n            * `https://ipfs.io` still vulnerable to network-related interference (i.e. DNS changes)\r\n            * Nothing enforces that `/ipfs` is used by `ipfs mount`\r\n    * **Option 2**: Disable all remote imports\r\n        * this prevents Dhall as a denial-of-service vector\r\n        * this prevents Dhall from leaking information through `GET` requests\r\n        * this prevents Dhall from leaking information through support for custom headers\r\n    * **Option 3**: Disable all imports\r\n        * this makes Dhall 100% pure\r\n        * this prevents Dhall from being tricked into an infinite import loop by malicious hosts\r\n            * i.e. `http://example.com/1 → http://example.com/2 → http://example.com/3 → ...`\r\n* Normalization-related safety:\r\n    * **Option 4**: Enforce that the input expression must already be in normal form\r\n        * This gives a linear upper bound on how long it takes to interpret a configuration file\r\n        * People who prefer this option either:\r\n            * Don't want to use Dhall as a programming language at all, or:\r\n            * Want to resolve/normalize Dhall expressions ahead-of-time\r\n\r\nMitigating factors:\r\n\r\n* Dhall has one built-in safety feature, which is that remote imports cannot reference local imports (i.e paths and environment variables)\r\n* The only IO that Dhall permits is imports\r\n\r\nThe Dhall API already supports all of the above features and they can all be implemented in linear time.  The main question is what *should* the command-line API support and what should the granularity of the API be\r\n\r\nFor example, one extreme is that the compiler just adds one new `--safe` flag which enforces the maximum possible safety by banning all imports and enforcing that the expression is in normal form.  This is simple but some users might want a solution with an intermediate amount of safety.\r\n\r\nAnother extreme is that we add four new flags (for each of the above options), which bloats the command-line API but satisfies everybody's use cases (that I'm aware of)"},"comment":{"url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/comments/352201876","html_url":"https://github.com/dhall-lang/dhall-haskell/issues/162#issuecomment-352201876","issue_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/162","id":352201876,"user":{"login":"Gabriel439","id":1313787,"avatar_url":"https://avatars3.githubusercontent.com/u/1313787?v=4","gravatar_id":"","url":"https://api.github.com/users/Gabriel439","html_url":"https://github.com/Gabriel439","followers_url":"https://api.github.com/users/Gabriel439/followers","following_url":"https://api.github.com/users/Gabriel439/following{/other_user}","gists_url":"https://api.github.com/users/Gabriel439/gists{/gist_id}","starred_url":"https://api.github.com/users/Gabriel439/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gabriel439/subscriptions","organizations_url":"https://api.github.com/users/Gabriel439/orgs","repos_url":"https://api.github.com/users/Gabriel439/repos","events_url":"https://api.github.com/users/Gabriel439/events{/privacy}","received_events_url":"https://api.github.com/users/Gabriel439/received_events","type":"User","site_admin":false},"created_at":"2017-12-16T18:34:02Z","updated_at":"2017-12-16T18:34:02Z","author_association":"COLLABORATOR","body":"So I took a stab at implementing `--normalized` and ran into one issue, which I can summarize with this tweet:\r\n\r\n<blockquote class=\"twitter-tweet\" data-lang=\"en\"><p lang=\"en\" dir=\"ltr\">Question for PLT people: if a System Fω expression is in normal form, can you type-check that expression in linear time (relative to the size of the expression, including types of bound variables)</p>&mdash; Gabriel Gonzalez (@GabrielG439) <a href=\"https://twitter.com/GabrielG439/status/942098064004616192?ref_src=twsrc%5Etfw\">December 16, 2017</a></blockquote>\r\n\r\nI'm going to hold off on implementing that flag until I know for sure the answer to that question\r\n"}}
{"actor":{"display_login":"Gabriel439"}}