biscuit: forbid unbound variables in rules and queries

The runtime makes them fail anyway, but it's better to catch
the error early: when parsing datalog or when deserializing
a token

biscuit/src/Auth/Biscuit/Datalog/AST.hs

@@ -75,10 +75,13 @@ module Auth.Biscuit.Datalog.AST
   , Authorizer' (..)
   , AuthorizerElement' (..)
   , ToEvaluation (..)
+  , makeRule
+  , makeQueryItem
   , checkToEvaluation
   , policyToEvaluation
   , elementToBlock
   , elementToAuthorizer
+  , extractVariables
   , fromStack
   , listSymbolsInBlock
   , listPublicKeysInBlock
@@ -111,9 +114,11 @@ import           Control.Monad              ((<=<))
 import           Data.ByteString            (ByteString)
 import           Data.ByteString.Base16     as Hex
 import           Data.Foldable              (fold, toList)
-import           Data.List.NonEmpty         (NonEmpty)
+import           Data.Function              (on)
+import           Data.List.NonEmpty         (NonEmpty, nonEmpty)
 import           Data.Map.Strict            (Map)
 import qualified Data.Map.Strict            as Map
+import           Data.Maybe                 (mapMaybe)
 import           Data.Set                   (Set)
 import qualified Data.Set                   as Set
 import           Data.String                (IsString)
@@ -125,7 +130,7 @@ import           Instances.TH.Lift          ()
 import           Language.Haskell.TH
 import           Language.Haskell.TH.Syntax
 import           Numeric.Natural            (Natural)
-import           Validation                 (Validation, failure)
+import           Validation                 (Validation (..), failure)
 
 import           Auth.Biscuit.Crypto        (PublicKey, pkBytes)
 
@@ -434,6 +439,19 @@ queryHasNoV4Operators :: Query -> Bool
 queryHasNoV4Operators =
   all (all expressionHasNoV4Operators . qExpressions)
 
+makeQueryItem :: [Predicate' 'InPredicate ctx]
+              -> [Expression' ctx]
+              -> Set (RuleScope' 'Repr ctx)
+              -> Validation (NonEmpty Text) (QueryItem' 'Repr ctx)
+makeQueryItem qBody qExpressions qScope =
+  let boundVariables = extractVariables qBody
+      exprVariables = foldMap extractExprVariables qExpressions
+      unboundVariables = exprVariables `Set.difference` boundVariables
+   in case nonEmpty (Set.toList unboundVariables) of
+        Nothing -> pure QueryItem{..}
+        Just vs -> Failure vs
+
+
 data CheckKind = One | All
   deriving (Eq, Show, Ord, Lift)
 
@@ -600,6 +618,38 @@ listSymbolsInRule Rule{..} =
 listPublicKeysInRule :: Rule -> Set.Set PublicKey
 listPublicKeysInRule Rule{scope} = listPublicKeysInScope scope
 
+extractVariables :: [Predicate' 'InPredicate ctx] -> Set Text
+extractVariables predicates =
+  let keepVariable = \case
+        Variable name -> Just name
+        _             -> Nothing
+      extractVariables' Predicate{terms} = mapMaybe keepVariable terms
+   in Set.fromList $ extractVariables' =<< predicates
+
+extractExprVariables :: Expression' ctx -> Set Text
+extractExprVariables =
+  let keepVariable = \case
+        Variable name -> Set.singleton name
+        _             -> Set.empty
+   in \case
+        EValue t       -> keepVariable t
+        EUnary _ e     -> extractExprVariables e
+        EBinary _ e e' -> ((<>) `on` extractExprVariables) e e'
+
+makeRule :: Predicate' 'InPredicate ctx
+         -> [Predicate' 'InPredicate ctx]
+         -> [Expression' ctx]
+         -> Set (RuleScope' 'Repr ctx)
+         -> Validation (NonEmpty Text) (Rule' 'Repr ctx)
+makeRule rhead body expressions scope =
+  let boundVariables = extractVariables body
+      exprVariables = foldMap extractExprVariables expressions
+      headVariables = extractVariables [rhead]
+      unboundVariables = (headVariables `Set.union` exprVariables) `Set.difference` boundVariables
+   in case nonEmpty (Set.toList unboundVariables) of
+        Nothing -> pure Rule{..}
+        Just vs -> Failure vs
+
 data Unary =
     Negate
   | Parens

biscuit/src/Auth/Biscuit/Datalog/Executor.hs

@@ -28,8 +28,6 @@ module Auth.Biscuit.Datalog.Executor
   , keepAuthorized'
   , defaultLimits
   , evaluateExpression
-  , extractVariables
-
   --
   , getFactsForRule
   , checkCheck
@@ -259,15 +257,6 @@ satisfies :: Limits
           -> Bool
 satisfies l b e = evaluateExpression l (snd b) e == Right (LBool True)
 
-extractVariables :: [Predicate] -> Set Name
-extractVariables predicates =
-  let keepVariable = \case
-        Variable name -> Just name
-        _             -> Nothing
-      extractVariables' Predicate{terms} = mapMaybe keepVariable terms
-   in Set.fromList $ extractVariables' =<< predicates
-
-
 applyBindings :: Predicate -> Scoped Bindings -> Maybe (Scoped Fact)
 applyBindings p@Predicate{terms} (origins, bindings) =
   let newTerms = traverse replaceTerm terms

biscuit/src/Auth/Biscuit/Datalog/Parser.hs

@@ -24,6 +24,7 @@ import qualified Data.ByteString.Char8          as C8
 import           Data.Char
 import           Data.Either                    (partitionEithers)
 import           Data.List.NonEmpty             (NonEmpty)
+import qualified Data.List.NonEmpty             as NE
 import           Data.Map.Strict                (Map)
 import           Data.Maybe                     (isJust)
 import           Data.Set                       (Set)
@@ -39,7 +40,8 @@ import           Language.Haskell.TH.Syntax     (Lift)
 import           Text.Megaparsec
 import qualified Text.Megaparsec.Char           as C
 import qualified Text.Megaparsec.Char.Lexer     as L
-import           Validation                     (Validation, validationToEither)
+import           Validation                     (Validation (..),
+                                                 validationToEither)
 
 type Parser = Parsec SemanticError Text
 
@@ -51,6 +53,7 @@ data SemanticError =
   | NestedSet Span
   | InvalidBs Text Span
   | InvalidPublicKey Text Span
+  | UnboundVariables (NonEmpty Text) Span
   deriving stock (Eq, Ord)
 
 instance ShowErrorComponent SemanticError where
@@ -60,6 +63,7 @@ instance ShowErrorComponent SemanticError where
     NestedSet _          -> "Sets cannot be nested"
     InvalidBs e _        -> "Invalid bytestring literal: " <> T.unpack e
     InvalidPublicKey e _ -> "Invalid public key: " <> T.unpack e
+    UnboundVariables e _ -> "Unbound variables: " <> T.unpack (T.intercalate ", " $ NE.toList e)
 
 run :: Parser a -> Text -> Either String a
 run p = first errorBundlePretty . runParser (l (pure ()) *> l p <* eof) ""
@@ -285,10 +289,14 @@ exprTerm = choice
 
 ruleParser :: Parser (Rule' 'Repr 'WithSlices)
 ruleParser = do
+  begin <- getOffset
   rhead <- l predicateParser
   _ <- l $ chunk "<-"
   (body, expressions, scope) <- ruleBodyParser
-  pure Rule{rhead, body, expressions, scope }
+  end <- getOffset
+  case makeRule rhead body expressions scope of
+    Failure vs -> registerError (UnboundVariables vs) (begin, end)
+    Success r  -> pure r
 
 ruleBodyParser :: Parser ([Predicate' 'InPredicate 'WithSlices], [Expression' 'WithSlices], Set.Set (RuleScope' 'Repr 'WithSlices))
 ruleBodyParser = do
@@ -314,10 +322,16 @@ scopeParser = do
    in Set.fromList <$> sepBy1 (l elemParser)
                               (l $ C.char ',')
 
+queryItemParser :: Parser (QueryItem' 'Repr 'WithSlices)
+queryItemParser = do
+  (sp, (predicates, expressions, scope)) <- getSpan ruleBodyParser
+  case makeQueryItem predicates expressions scope of
+    Failure e  -> registerError (UnboundVariables e) sp
+    Success qi -> pure qi
+
 queryParser :: Parser [QueryItem' 'Repr 'WithSlices]
 queryParser =
-  let mkQueryItem (qBody, qExpressions, qScope) = QueryItem { qBody, qExpressions, qScope }
-   in fmap mkQueryItem <$> sepBy1 ruleBodyParser (l $ C.string' "or" <* C.space)
+   sepBy1 queryItemParser (l $ C.string' "or" <* C.space)
 
 checkParser :: Parser (Check' 'Repr 'WithSlices)
 checkParser = do

biscuit/src/Auth/Biscuit/Datalog/ScopedExecutor.hs

@@ -50,7 +50,6 @@ import           Auth.Biscuit.Datalog.Executor (Bindings, ExecutionError (..),
                                                 ResultError (..), Scoped,
                                                 checkCheck, checkPolicy,
                                                 countFacts, defaultLimits,
-                                                extractVariables,
                                                 fromScopedFacts,
                                                 getBindingsForRuleBody,
                                                 getFactsForRule,

biscuit/test/Spec/Parser.hs

@@ -76,6 +76,7 @@ specs = testGroup "datalog parser"
   , constraints
   , constrainedRule
   , constrainedRuleOrdering
+  , ruleVariables
   , ruleWithScopeParsing
   , checkParsing
   , policyParsing
@@ -327,6 +328,25 @@ operatorPrecedences = testGroup "mixed-precedence operators"
               )
   ]
 
+ruleVariables :: TestTree
+ruleVariables = testGroup "Make sure rule & query variables are correctly introduced"
+  [ testCase "Head variables are correctly introduced" $
+      parseRule "head($unbound) <- body(true)" @?=
+        Left "1:1:\n  |\n1 | head($unbound) <- body(true)\n  | ^\nUnbound variables: unbound\n"
+  , testCase "Expression variables are correctly introduced (rule)" $
+      parseRule "head(true) <- body(true), $unbound" @?=
+        Left "1:1:\n  |\n1 | head(true) <- body(true), $unbound\n  | ^\nUnbound variables: unbound\n"
+  , testCase "Expression variables are correctly introduced (check)" $
+      first mempty (parseRule "check if body(true), $unbound") @?=
+        Left ()
+  , testCase "Expression variables are correctly introduced (allow policy)" $
+      first mempty (parseRule "allow if body(true), $unbound") @?=
+        Left ()
+  , testCase "Expression variables are correctly introduced (deny policy)" $
+      first mempty (parseRule "deny if body(true), $unbound") @?=
+        Left ()
+  ]
+
 ruleWithScopeParsing :: TestTree
 ruleWithScopeParsing = testCase "Parse constained rule with scope annotation" $
   parseRule "valid_date(\"file1\") <- time($0), resource(\"file1\"), $0 <= 2019-12-04T09:46:41+00:00 trusting previous" @?=

biscuit/test/Spec/SampleReader.hs

@@ -192,14 +192,18 @@ checkTokenBlocks step b blockDescs = do
 processTestCase :: (String -> IO ())
                 -> PublicKey -> TestCase (FilePath, ByteString)
                 -> Assertion
-processTestCase step rootPk TestCase{..} = do
-  step "Parsing "
-  let vList = Map.toList validations
-  case parse rootPk (snd filename) of
-    Left parseError -> traverse_ (processFailedValidation step parseError) vList
-    Right biscuit   -> do
-      checkTokenBlocks step biscuit token
-      traverse_ (processValidation step biscuit) vList
+processTestCase step rootPk TestCase{..} =
+  if fst filename == "test018_unbound_variables_in_rule.bc"
+  then
+    step "Skipping for now (unbound variables are now caught before evaluation)"
+  else do
+    step "Parsing "
+    let vList = Map.toList validations
+    case parse rootPk (snd filename) of
+      Left parseError -> traverse_ (processFailedValidation step parseError) vList
+      Right biscuit   -> do
+        checkTokenBlocks step biscuit token
+        traverse_ (processValidation step biscuit) vList
 
 compareParseErrors :: ParseError -> RustError -> Assertion
 compareParseErrors pe re =

biscuit/test/Spec/Verification.hs

@@ -11,10 +11,12 @@ import           Test.Tasty
 import           Test.Tasty.HUnit
 
 import           Auth.Biscuit
-import           Auth.Biscuit.Datalog.AST      (Check, Check' (..),
+import           Auth.Biscuit.Datalog.AST      (Block' (..), Check, Check' (..),
                                                 CheckKind (..),
-                                                Expression' (..), Query,
-                                                QueryItem' (..), Term' (..))
+                                                Expression' (..),
+                                                Predicate' (..), Query,
+                                                QueryItem' (..), Rule' (..),
+                                                Term' (..))
 import           Auth.Biscuit.Datalog.Executor (MatchedQuery (..),
                                                 ResultError (..))
 import qualified Auth.Biscuit.Datalog.Executor as Executor
@@ -87,7 +89,27 @@ unboundVarRule :: TestTree
 unboundVarRule = testCase "Rule with unbound variable" $ do
   secret <- newSecret
   b1 <- mkBiscuit secret [block|check if operation("read");|]
-  b2 <- addBlock [block|operation($unbound, "read") <- operation($any1, $any2);|] b1
+  -- rules with unbound variables don't parse, so we have
+  -- to manually construct a broken rule
+  let brokenRuleBlock = Block {
+        bRules = [Rule{
+          rhead = Predicate{
+            name = "operation",
+            terms = [Variable"unbound", LString "read"]
+          },
+          body = [Predicate{
+            name = "operation",
+            terms = Variable <$> ["any1", "any2"]
+          }],
+          expressions = mempty,
+          scope = mempty
+        }],
+        bFacts = mempty,
+        bChecks = mempty,
+        bScope = mempty,
+        bContext = mempty
+  }
+  b2 <- addBlock brokenRuleBlock b1
   res <- authorizeBiscuit b2 [authorizer|operation("write");allow if true;|]
   res @?= Left InvalidRule