Dhall – A Distributed, Safe Configuration Language
github.com
github.com
If you need some example of use cases to see if it might help you, check out "Dhall in Production" [0]
So far I'm a maintainer of dhall-kubernetes [1] and we'll soon open source some of our integration with Terraform.
And because it's absolutely safe to distribute Dhall code I'm toying with the idea of making some kind of Dhall-Kafka pubsub, in which you can safely distribute Dhall code and data, with automatic version migrations (check this out for more info on why this is possible [2])
[0]: https://github.com/dhall-lang/dhall-lang/wiki/Dhall-in-produ...
[1]: https://github.com/dhall-lang/dhall-kubernetes
[2]: http://www.haskellforall.com/2017/11/semantic-integrity-chec...
Dhall seems to be safe in the sense that it will always terminate and will never crash or throw some kind of exception, but I don't think it's safe in the sense that it is safe to execute potentially malicious Dhall code, unless you restrict the allowed imports to a whitelist.
At the very least that could be used to DDos some target by having the script try to import something from a victim domain. And you might be able to read data on local files and transmit that information back, I'm not sure. It depends on if imports are evaluated lazily, and the data of interest would have to be stored in a file on disk that can be imported.
EDIT: Actually, it looks like you can import raw text, so it doesn't matter what format the on-disk data is that you are trying to extract.
EDIT2: Actually, it doesn't even matter if imports are evaluated lazily or not, you can specify that a network import be made with given headers, so you could just set a header in the HTTP request to contain the sensitive data.
https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...
The main risks in executing potentially malicious Dhall code that is not protected by a semantic integrity check are:
* Using more computer resources than you expected (i.e. network/CPU/RAM)
* Unintentional DDos (as you mentioned)
* The malicious import returning a value which changes the behavior of your program
If you protect the import with a semantic integrity check then the malicious import can no longer return an unexpected value, which eliminates the third issue (changing program behavior). Also, upcoming versions will cache imports based on the semantic integrity check, which would mitigate the second issue (DDos) for all but the first time you interpret the program. There is also a `dhall freeze` subcommand which takes a program and automatically pins imports to their most recent value using semantic integrity check.
Regarding exfiltration, the import system guarantees that only local imports can access sensitive information such as file contents or environment variables. See:
https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...
The only way that a remote import can obtain that information is if a local import supplied that information via Dhall's support for custom headers. In fact, this is actually an intended use of that feature (i.e. a local import fetching a Dhall expression from a private GitHub repository using an access token retrieved from an environment variable).
So in other words the threat model is that as long as you can trust local imports then you can transitively trust remote imports because they cannot access your local filesystem or environment variables unless you explicitly opt into that via a local import. I think that's a reasonable threat model because if can't trust the contents of your local filesystem then you can't even trust the Dhall interpreter that you are using :)
Imports are not computed and the set of imports that you retrieve is static (i.e. does not change in response to program state or input), so the set of imports or their paths cannot be used as an exfiltration vector.
Seriously great work on this, by the way. A total configuration language that allows some form of network access while still being secure against malicious input is a really really impressive tool!
Yes, a local import would be able to access an intranet site and re-export that information via custom headers supplied to another import. This is allowed because it falls under trusting local imports. Local imports have access to environment variables and your local filesystem, too, which are equally sensitive, which is why they need to be trusted.
This rule is called the "referential transparency" check, which can be summed up as:
* Only environment variables, absolute paths, and home-anchored paths classify as "local" imports
* Only local imports can retrieve other local imports
* URLs can import relative paths, but they are relative to the URL, not relative to your local filesystem
The reason it's called the "referential transparency" check is because this security restriction also leads to the nice property that import system is referentially transparent. That means that every import evaluates to the same result no matter you import it from. For example, if you have a directory of Dhall expressions that refer to each other and you rehost them on a file server the language guarantees that they still behave the same whether you import them locally or you import them via their hosted URLs.
Also, thanks! :)
If you wanted to generate something like an NGINX config (or, for example, TOML or Terraform) you could use dhall-text: https://github.com/dhall-lang/dhall-text
Oh, did I say terraform? Someone's already on supporting that directly: https://github.com/blast-hardcheese/dhall-terraform
Dhall is very unique among configuration because it's "distributed", meaning that Dhall can load any file as a dhall expression, and has builtin URI resolvers to make even remote endpoints part of local configuration. This is excellent for, say, CI integration.
Dhall has "semantic hashing" so that if someone does change a dhall dependency in a surprising way, the dhall script will refuse to continue (and give a very clear error about what changed, where it was looking for the change, and why it's stopping).
Dhall is a secret superpower for project configuration. Especially as of the 1.14+ releases, it's become an increasingly go-to tool for me. Even in just one-off JSON generation scripts, I find it to be a lifesaver.
$ nix-instantiate --eval --read-write-mode -E 'Nix code goes here'
That Nix code could be a file, or an import, or whatever. This is slightly improved with Nix 2.x: $ nix eval '(Nix code goes here)'
Still, it's not particularly well suited to string processing from the commandline like this. We're closer to Nix's comfortable territory if we use it to build a config file, e.g. $ nix-build -E 'Nix code goes here'
Or, more likely: $ nix-build myConfigFileDescription.nix
In my experience this is more useful than trying to use Nix as a string processor. Still, if we're using Nix in a project or system, we might be better off using it to build the whole project (e.g. with a 'default.nix' file) or system (using a NixOS module or something).From what I've seen, Guix takes compatibility with non-Guix systems a little closer to heart, e.g. for generating standalone packages that don't require Guix to install/use.
Do you happen to know of any?
Perhaps you're looking for something with even more features and applicability (e.g. an example of a Kubernetes config as Dhall's author points out), but hopefully that example gives at least a self-contained example of how to gradually start using Dhall.
I saw that lists can have only one type of elements without annotating their types. With type annotation list can have differently typed values, but only if each element is explicitly stated (note: this is my understanding that might not be correct) meaning there's no dynamic content in a list. In same vein a map of maps needs to have all its keys stated by type annotation.
To me this seems too restrictive since the structure of data gets lost in the more verbose annotations. Not to mention the work of writing this annotation or the functionality to produce the same. In TypeScript I'd write something like this { [string] : [ Number | String ] } and I'd have my string keyed object with values of lists containing numbers and strings. Having a language like Dhall to help with creation of correct configuration code seems really useful instead of this messy combination of declarative and template language. I would like to understand things that can get better by using such an type system.
You only need to annotate the type of an empty list. Lists with at least one element don't require a type annotation because the type can be inferred from the type of that element.
Dhall does not have buit-in support for homogeneous maps. Dhall does have statically typed heterogeneous records (i.e. something like `{ foo = Bool, bar = "ABC" }` which has type `{ foo : Bool, bar : Text }` for example).
If you want to store different type of values in the same list you wrap them in a union. For example, if you want to store both `Text` values and `Natural` numbers in a list you would do:
let union = constructors < Left : Natural | Right : Text >
in [ union.Left 10, union.Right "ABC", union.Right "DEF", union.Left 4 ]
The closest thing to a homogeneous map in Dhall is an association list of type `[ { mapKey : Text, mapValue : a } ]` but even that is still not an exact fit since it doesn't guarantee uniqueness of keys. However, Dhall's JSON/YAML integration does convert that automatically to a JSON/YAML homogeneous map (i.e. a JSON record where every field has the same type).In general, Dhall's JSON/YAML integration has several tricks and conventions that translate to weakly typed JSON idioms (such as homogeneous maps, omitting null values, and using tags).
This Left and Right declaration style was a new one for me. Also, homogeneous map wasn't exactly a familiar concept. I don't remember meeting these when learning TypeScript and dabbling with Elm. I fear I don't quite grasp the type structure here yet. I can go forward with my testing based on your example.
And by the way, TypeScript DOES have a form of Sum typing like that as of 2017! You can say something like this from the manual:
type Shape = Square | Rectangle | Circle | Triangle;
function area(s: Shape) {
switch (s.kind) {
case "square": return s.size * s.size;
case "rectangle": return s.height * s.width;
case "circle": return Math.PI * s.radius ** 2;
}
// should error here - we didn't handle case "triangle"
}
(You can see more about it here: https://www.typescriptlang.org/docs/handbook/advanced-types...., search for "Discriminated Unions".)You can also make these ad-hoc ,and they're useful for harnessing underlying functions that might return null from stdlibs. E.g.,
function strToInt( x: string ): number | null
And then you're required to check for nulls and the compiler will complain if you don't check for them. Pretty useful!Jsonnet strikes a great balance of json but with some nice template syntax so you can be DRY.
Also what’s wrong with being Turing complete. I love for loops.
However, if you do want to type them then see:
https://en.wikipedia.org/wiki/Unicode_input
... and the relevant code points are:
* `λ`: `U+03BB`
* `∀`: `U+2200`
So for example, in your configuration, you can define a common expression into a variable (or even parametrize it in a function). CL:read cannot do that without resorting to read macros (technically it doesn't have to be read macros, you can reinterpret it later, but then we are getting outside the realm of CL:read), which are Turing complete and can have bugs that can lead to security exploits.
Dhall guarantees that the functions you define in your configuration cannot be exploited.
This has interesting implications, for example, you can read configuration safely from semi-trusted source. With CL:read, you can do that only if you give up read macros, but then the semi-trusted source cannot define their own function.
So where with CL:read you have to choose between little and total power, Dhall gives you a little bit of both, a medium power of sorts.
Similar to YAML. Too much power, recursive via links, too insecure.
This is of course biased, unresearched anecdata but roughly speaking
- 50 % of all IT installations cannot be rebuilt from scratch in an automated fashion if you have them the new hardware,plugged in.
A further ten percent could be rebuilt with mostly automated scripts and a wiki page that's out of date by two months
of the remaining 1/3 of the world's IT, 1/6 has dependencies it does not know about - the DNS server that "just works",the production routers that should not serve that subnet, the database that is "owned" by a different team whose configuration you have no control over.
Good guy d.b. has its secret passwords on the wiki page, or stored on a seperate importable module, in source control, base64-encoded
And the rest - the rest rely more on bash than ansible.
Just get the world's enterprise services over the line and into "run this python script with these parma's and you get a complete rebuild across databases and routers" and then we can talk.
On the other hand, I can use Dhall to generate Kubernetes/Helm configs, which will be more DRY, less duplicated, and not a pain to work with. I know that this would help me quite a bit, not only because I hate my current "DevOps" team members with burning passion and I'd enjoy watching them try to figure out what is happening (well, I'd at least add the source files to a repo, that's already more than they do).
The convoy has wagons with broken spikes, no horses and people berating them because they are not travelling as fast as the well maintained ones in front
Shed a tear for those being carried by such wagons - they could reach the future so much faster if best practises were common practises
And this from someone who believes in Schumpter
This is an excessively negative argument, and has been used many times to push back against technologies that have subsequently shown to actually have huge traction. A great example of this that the Python community still makes: lambdas are too complicated.
I don't think there is an OSS solution for a team that is working on five year old RHEL, differently configured servers and half the deployment is done by a different team in a different continent. This is just the default for an awful lot of the enterprise world, (no one designed it like that - it's just how internal politics got them there) and when you hit the SME world "it's been up and working for two years, we won't look too closely"
I am not trying to be sarcastic or defeatist- just trying to assess reality. I am positive - this can be solved globally with really cool tools but the tools themselves do not drive their own adoption.
Simple things like Docker is the thing most likely to solve most of this - yet it's enterprise adoption seems to be awfully slow (needs root? not in my data centre).
But if there is a solution it is not technology - it is diktat. If every board of every company adopted one rule "You must be able to automatedly deploy a pre-prod environment that passes all automated tests, using the same scripts as the production deployment, changing only one configuration file" then world wide IT professional would leap a generation ahead.