Liquid Haskell误判Haskell JSON服务安全性，求排查解决

Hey there! Let’s figure out why your Liquid Haskell setup isn’t catching those partial function crashes in your Scotty JSON server, and how to fix this gap between static checking and runtime behavior.

I’ll fill in the missing bits of your code to match the common scenario where partial functions cause crashes—like using fromJust on a JSON decode result or relying on Scotty’s param without handling missing/invalid values:

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}
module Main where

import qualified Web.Scotty as Scot
import GHC.Generics (Generic)
import qualified Data.Aeson as Json
import Data.Text.Lazy (Text)
import Data.Maybe (fromJust)

data User = User { name :: Text, age :: Int } deriving (Generic, Show)
instance Json.FromJSON User

main :: IO ()
main = Scot.scotty 3000 $ do
  Scot.get "/user/:userId" $ do
    userId <- Scot.param "userId"  -- Partial: crashes if param is missing/invalid
    rawJson <- Scot.body
    let user = fromJust $ Json.decode rawJson  -- Partial: crashes if JSON is invalid
    Scot.text $ "Got user: " <> Scot.showText user

Liquid Haskell (LH) doesn’t catch partial functions by default for a few key reasons:

• No built-in contracts for third-party functions: LH relies on annotated libraries to know when a function is unsafe. Scotty’s param and Aeson’s decode (which returns Maybe) don’t come with default LH refinements, so LH doesn’t recognize their partial behavior.
• Unenforced Maybe constraints: When you use fromJust, LH won’t complain unless you’ve explicitly told it that the Maybe value is guaranteed to be Just a. Without that refinement, LH assumes the value could be Nothing but doesn’t flag the unsafe unwrap.
• Missing LH directives: Your code doesn’t enable strict checking or add refinement types to enforce valid inputs (like ensuring the route param exists or the JSON is well-formed).

Let’s walk through actionable steps to close this gap:

1. Ditch Partial Functions for Safe Alternatives #

Replace fromJust and Scotty’s param with their safe counterparts, then handle error cases explicitly. This not only fixes runtime crashes but also gives LH something to validate:

main :: IO ()
main = Scot.scotty 3000 $ do
  Scot.get "/user/:userId" $ do
    -- Use paramMaybe instead of param to get a Maybe value
    mUserId <- Scot.paramMaybe "userId"
    case mUserId of
      Just userId -> do
        rawJson <- Scot.body
        -- Pattern match on decode result instead of using fromJust
        case Json.decode rawJson of
          Just user -> Scot.text $ "Got user: " <> Scot.showText user
          Nothing -> Scot.status Scot.status400 >> Scot.text "Invalid JSON body"
      Nothing -> Scot.status Scot.status404 >> Scot.text "Missing or invalid user ID"

2. Add Liquid Haskell Annotations for Strict Checking #

Enable strict LH checks at the top of your file to force it to flag unsafe patterns:

{-@ LIQUID "--strict" @-}
{-@ LIQUID "--no-termination" @-}  -- Scotty's server runs indefinitely, so disable termination checks
{-@ LIQUID "--exact-data-cons" @-}  -- Ensure LH respects data constructor invariants

3. Annotate Third-Party Functions (Optional but Powerful) #

If you want LH to enforce constraints on Scotty/Aeson functions directly, add custom refinement contracts. For example, you can define a safe wrapper for decode that requires valid JSON:

{-# LANGUAGE TemplateHaskell #-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}

import LiquidHaskell

-- Define a refinement for non-null Maybe values
{-@ type Just a = {v:Maybe a | isJust v} @-}

-- Safe decode wrapper with a refinement (you'll need to validate inputs to use this)
{-@ safeDecode :: Json.FromJSON a => {bs:Scot.Body | isValidJSON bs} -> Just a @-}
safeDecode :: Json.FromJSON a => Scot.Body -> Maybe a
safeDecode = Json.decode

Note: To use this, you’d need to add a predicate isValidJSON that LH can verify, or pair it with input validation logic that proves the JSON is valid.

Liquid Haskell isn’t a magic bullet—you need to give it hints to catch unsafe code. By replacing partial functions with safe alternatives, handling error cases explicitly, and enabling strict checking, you’ll get the runtime safety you expect alongside LH’s static validation.

内容的提问来源于stack exchange，提问作者8n8