Datalog restrictions in blocks

[clementd-fretlink]

Currently, blocks can be added to any non-sealed biscuit. A block can contain both caveats (like in macaroons), but also facts and rules. This requires careful thought from both the biscuit minter and the biscuit verifier: the goal is to avoid confusing facts from the biscuit minter and facts from blocks.

To that end, the special #authority atom is used.
It's special in two ways:

• it's forbidden in blocks rules and facts
• it's automatically added in authority facts (and rules? not sure)

All that makes the semantics rather complex (and way more complex than, say, macaroons). Another possibility would be to completely forbid rules and facts in blocks, and only allow caveats. This would bring the attenuation semantics closer to those of macaroons, which are arguably easier to reason about.

I still see the value in more complexity in blocks, but I think it should be optional (ideally, opt-in). In that case, i think the biscuit should carry this information when minted. This would avoid validating an restricted biscuit with a verifier that expects an unrestricted one.

All in all, while datalog brings huge improvements over macaroons (putting aside asymmetric crypto), the ability to add rules and facts in blocks make the complexity explode and make auditing biscuits properties way harder.

As an additional bonus, not allowing rules in biscuits completely remove an attack channel where a legitimate biscuit is attenuated with rules crafted to exploit the datalog engine.

[Geal]

as mentioned in #59, the authority block could be a special case for deserialization, containing configuration data that other blocks cannot hold, such as this option

[svvac]

If the version at https://play-with-biscuit.cleverapps.io/ is up-to-date, the #authority and #ambient restrictions can easily be bypassed by any party able to create a new block.

This in turn allows to bypass any checks already present on the previous blocks or in the authority section. Conversely, with knowledge of the verifier code, one could craft a block that always grants passage.

[Geal]

@svvac could you explain how it is easily bypassed? Wth the playground, you cannot create a token with authority or ambient facts in blocks other than block 0.

Sure, it is possible to manually create a token with the authority or ambient tag by tweaking the library, but verifier implementations are supposed to refuse them. There's even one of the samples that test for that: https://github.com/CleverCloud/biscuit/tree/master/samples/v1#invalid-block-fact-with-authority-tag-test7_invalid_block_fact_authoritybc

Though if you have specific concerns or vulnerabilities to demonstrate, I'm always interested, I'll make sure to fix them quickly

[svvac]

@Geal Given the Files example, without touching the authority and first block, adding the following block results in Success for all values of resource(#ambient, *) and operation(#ambient, *) in the verifier:

// Bypass `check if operation(#ambient, #read)` from authority block
operation($ambient, #read) <- operation($ambient, $any);

// Bypass `check if resource(#ambient, $file), $file.starts_with("/folder1/")` from block #1
resource($ambient, "/folder1/") <- resource($ambient, $any);

// Add missing rights
right($authority, $file, $right) <- right($authority, $any1, $any2), resource(#ambient, $file), operation(#ambient, $right);

Also different issue (I think), but with the same effect : there seems to be a bug where leftover variables in the rule pattern matches the #authority symbol:

// Bypass `check if operation(#ambient, #read)` from authority block
operation($unbound, #read) <- operation($any1, $any2);

// Bypass `check if resource(#ambient, $file), $file.starts_with("/folder1/")` from block #1
resource($unbound, "/folder1/") <- resource($any1, $any2);

// Add missing rights
right($unbound, $file, #read) <- resource($any1, $file);

[Geal]

Nice catch, thanks, I'll fix that and add a new sample to verify that behaviour

[Geal]

@svvac the bugs were identified and fixed in the Rust and Java implementation, soon in the Go one, and I have prepared test samples to test that for future implementations. The fixes should be pushed soon. I'll announce the vulnerabilities and make a changelog. Do you want to be credited in the announcement?

[svvac]

@Geal I don't mind, thanks for asking. Glad to hear it got fixed fast.

[Geal]

I'm waiting on a few updates before publishing about it, but Rust and Java versions are available with the fix

[divarvel]

Special atoms are no longer needed to scope facts.