Add pure version of authorizeBiscuit

[kephas]

A lot of biscuit's functions that require IO or MonadIO could have either pure versions or versions that could run in a wider range of monads. authorizeBiscuit may be the simplest because its only dependency on IO is because of timer.

This would still require documenting that it must be run in a context where a bad biscuit wouldn't make authorizeBiscuitNoTimeout run for an extended time.

[divarvel]

Thanks!

I guess that apart from authorize, the other candidates are all functions depending on keypair generation, which could indeed be relaxed to MonadRandom.

Do note that there is planned support for ECDSA, which would turn some currently pure operations into monadic ones (but it should only add a MonadRandom constraint, not full-on IO)

[divarvel]

on one hand it might be possible to extract this common code in a helper function, but OTOH it's just plumbing with no important logic in it so it's not too big an issue.

[kephas]

Yeah, this PR was more a proof-of-concept than a definitive alternative. I wondered if it would be better to factor out the common parts but I went for the easiest path first.

[kephas]

The common part could be authorizeBiscuitWithRunner :: Functor f => (Limits -> BlockWithRevocationId -> [BlockWithRevocationId] -> Authorizer -> f (Either ExecutionError AuthorizationSuccess)) -> Limits -> Biscuit proof Verified -> Authorizer -> f (Either ExecutionError (AuthorizedBiscuit proof)) and it would have the exact same code as the current authorizeBiscuitWithLimits with runAuthorizerWithLimits replaced by the first argument.

Then authorizeBiscuitWithLimitsNoTimeout = unIdentity . authorizeBiscuitWithRunner runAuthorizerNoTimeout…

[divarvel]

Yes, that's what I had in mind

[kephas]

I added it to the PR.

[divarvel]

could you add a haddoc comment explaining its purpose and outlining the danger?
it might good to refer to it from the doc items of authorizeBiscuitWithLimits

[kephas]

I know Prolog can easily have infinite loops but I don't know about Datalog or the way it's evaluated in Biscuit, so I'll write the doc warning about that too.

[divarvel]

The semantics for this Datalog flavour means it always converges, so it's not about infinite loops per se, but about ensuring that it does within an acceptable duration

[kephas]

Comment fixed.

[kephas]

BTW, our use case is that we have Polysemy actions running in Servant, and it's not yet clear to us where we'd better validate or generate biscuits in our code, but the current implementation would force us to only use functions from biscuit-haskell in IO interpreters.

Having functions that only require MonadRandom would give us more options.

[divarvel]

BTW, our use case is that we have Polysemy actions running in Servant

Have you looked at biscuit-servant yet? My plan was to try it out with an effect system (probably effecful rather than polysemy though).
Basically biscuit authorization is separated in two steps:

• first, parsing & signature verification : this happens in an auth handler that's provided through Context. Currently this part is polymorphic on the monad (verification itself is pure, but there is a revocation check provided by the caller that has an applicative constraint)
• then, authorization itself: it can happen either in a helper that you call in each endpoint and takes the handler code as a parameter, or in a natural transformation that you apply on all endpoints at the same time using hoistServer. IO is currently required here, and there are functions used in this context that can introduce a polymorphic monad constraint (when generating the authorizer requires effects: eg getting the current datetime), but there is still a monadio constraint.

Disabling an important check to please an effect system seems a bit dangerous to me. OTOH relaxing IO to MonadRandom for key generation preserves semantics and would unlock nice use cases.

It might be possible to declare the timeout check in a specific typeclass implemented by IO (the actual impl requires getCurrentTime and forkIO amongst other things) to make integrating with an effect system a bit easier

[kephas]

We are indeed looking at biscuit-servant. At first glance, it would seem useful if we can use biscuit verification without needing effects like Embed IO or Final IO in our effects. It's not the case yet, but I plan to have some interpreters interpret effects in STM, where we could easily provide MonadRandom.

Is there a way to help you try testing an effect system with biscuit-servant?

[divarvel]

We are indeed looking at biscuit-servant. At first glance, it would seem useful if we can use biscuit verification without needing effects like Embed IO or Final IO in our effects. It's not the case yet, but I plan to have some interpreters interpret effects in STM, where we could easily provide MonadRandom.

MonadRandom is only useful/needed for biscuit generation. IO is needed for timeout management during authorization.

Is there a way to help you try testing an effect system with biscuit-servant?

I don't use Haskell at work anymore so i might not have time to do that before a couple weeks.
I have used servant along effectful at my previous job, so i might try that.

That being said, all the servant helpers are polymorphic on the handler monad, so this should work with effects anyway.

Extracting the timeout check in a dedicated typeclass would make things easier if you want to forego timeouts (and IO) completely

[divarvel]

👋 I might have time to assist if you want to try and express the timeout check through a typeclass constraint, that could be discharged by IO itself, or by a dedicated effect.

[kephas]

Great! How would you want to proceed?

[divarvel]

Great! How would you want to proceed?

Once you have rebased the PR to fix conflicts, maybe we can pair-prog on it and try to come up with a typeclass that can be compatible with an effect system (ideally effectful and polysemy)

[kephas]

I think I'd be available enough in a few weeks to do that, that sounds like a plan.

[divarvel]

I’d be open to resuming working on this, based on #94, and providing an extension point designed for use with effect systems

[kephas]

Superseded by #104