“I added this feature in response to user concerns about code injection in Dhall configuration files.”
I’m going to have to pause here as I’m confused on threat model. I previously submitted something Dhall-related here since I like the concept. However, anyone with write access to the configuration files in an application directory or source usually has write access to the source or binaries of the application itself. We already have tools for mitigating this in terms of repos or system-level security. The attacker who can change the import can just change the hash in the Dhall configuration file or whatever at the Dhall-level is being used for security.
“This configuration imports a helper function named map from the Dhall Prelude by URL:”
First, author already decided to let that 3rd party to develop, supply and/or host the configuration. That third party is “trusted:” inherently a risk to security. Probably better to pull the configuration in manually, review it, and, if passed review, store it with whatever app will use it. Third party, their storage, transport and all of that is no longer a risk. Second, anything done over an untrusted network is best done with transport-level security instead of http used in example. Then, author doesn’t have to add anything to the programming language to deal with modifications in transit. If the 3rd party can’t pull off https, author may have bigger problems trusting them. If there’s legitimate reasons for no transport or storage security, there’s vetted encryption software to wrap it with such as GPG that should be used instead of homebrewing something. There’s even smartcards and stuff to reduce risk of endpoint compromises affecting integrity/authenticity in that case.
Note: Quick check shows the site supports HTTPS. Good it was a hypothetical example. Back to the technical stuff.
“Once you add these integrity checks the Dhall interpreter will enforce them when resolving imports. In this case, the example configuration still successfully evaluates to the same result after adding the integrity checks:”
It kind of reminds me of static typing with type-safe linking of modules. You say “this won’t change.” Then, anything extra you bring in has to conform to that. Just done with hashes instead. This might have value for ensuring correctness or debugging.
“These are semantic hashes, not textual hashes… For example, suppose that we modify…”
Interesting concept. Seems somewhat like integrity-checking a BNF grammar for a file to be parsed.
“even if we were to distribute the imported code over an insecure channel.”
Root of the problem again. Just don’t do that. Also, check all app dependencies that are being distributed at once in a zip file or something. It’s faster, it uses well-scrutinized software, and some CPU’s hardware accelerate those primitives. It’s also standard.
“A textual hash of the ./students.dhall import would not detect this change because the real change took place in the text of another file that ./students.dhall imported. “
I don’t know the language enough to evaluate refactoring claim. As I noted on correctness, it might be useful for that. However, this sounds like it could be solved preprocessor style where all the imports happen at a text level before the hash is applied. Nothing is necessarily executed: just text reads/downloads and insertions. If something went from a 2 to a 3, then the SHA-256 hash will be substantially different. So, I’m not sold on semantic over text versioning being necessary esp as we’ve made text/bit-based method work with about every application imaginable. Probably a good time to also push WYSIWYG philosophy of configuration files and data formats since that helps.
Dhall looks really interesting. After being burned by turing-complete configuration languages in previous projects, I’m glad someone has taken the time to tackle the problem seriously.