类型安全的Servant Auth角色
摘要
本文描述了在Haskell的servant-auth库基础上设计和实现的一种类型安全的基于角色的授权系统,该系统支持为每个角色设置不同的处理程序,并在编译时进行检查。
<p><a href="https://lobste.rs/s/wxq96p/type_safe_servant_auth_roles">评论</a></p>
查看缓存全文
缓存时间: 2026/07/20 17:27
# Servant 认证角色
来源:https://blog.cofree.coffee/2026-07-20-servant-auth-roles/
所罗门博客
函数式编程、永续农业、数学
我想在 `servant-auth` 之上创建一种优雅的角色系统。本文梳理了设计与实现过程。最终结果与 OCharle 的《Who Authorized These Ghosts》(https://blog.ocharles.org.uk/blog/posts/2019-08-09-who-authorized-these-ghosts.html) 非常相似。你可以在这里 (https://github.com/solomon-b/servant-auth-roles) 看到最终成果。
我直接想要的是在 Servant API 类型中实现认证角色/权限集,以便为每个认证角色定义不同的处理器。同时还要保持与 `AuthProtect` 的兼容性。
## 想法
第一步,勾勒出这个库的假想接口。我希望从接口出发,代码的实现方式会自然浮现。
我想将角色定义为一个和类型,然后实例化一个类型类来描述角色检查条件。这样我就可以设计各种角色体系(层级式、非层级式、基于集合等)。
```haskell
data UserRole = Viewer | Editor | Admin
deriving (Eq, Ord, Show)
instance CheckRole 'Viewer where
checkRole role = role >= Viewer
instance CheckRole 'Editor where
checkRole role = role >= Editor
instance CheckRole 'Admin where
checkRole role = role >= Admin
```
`CheckRole` 允许使用任意谓词。这里我使用了 `Ord`,因为我希望有传递性,但我们也可以直接使用 `Eq`,甚至使用集合成员关系(如果你要建模的是“权限”而非“角色”)。
然后我们定义典型的 Servant 认证类型和 `AuthServerData` 实例:
```haskell
data Authz = Authz { userRole :: UserRole, userName :: String }
deriving (Show)
type instance AuthServerData (AuthProtect "test-auth") = Authz
```
最后用一个神奇的 Servant 组合子 `RequireRole`,我可以在 API 类型中用它为路由分配认证角色。该组合子会在处理器执行前引入一个角色权限检查。如果 `Authz` 中的 `UserRole` 值不满足处理器的 `RoleCheck`,则检查失败,并尝试下一个匹配的路由。
```haskell
type PanelAdminAPI =
RequireRole "test-auth" 'Admin
:> "panel"
:> Get '[JSON] String
type PanelEditorAPI =
RequireRole "test-auth" 'Editor
:> "panel"
:> Get '[JSON] String
type PanelViewerAPI =
RequireRole "test-auth" 'Viewer
:> "panel"
:> Get '[JSON] String
type API = PanelAdminAPI :<|> PanelEditorAPI :<|> PanelViewerAPI
server :: Server API
server = panelAdmin :<|> panelEditor :<|> panelViewer
where
panelAdmin :: Authz -> Handler String
panelAdmin _ = pure "admin panel"
panelEditor :: Authz -> Handler String
panelEditor _ = pure "editor panel"
panelViewer :: Authz -> Handler String
panelViewer _ = pure "viewer panel"
```
显然这还不能直接工作,但我希望开发者体验大致如此。
## 让想法变为现实
实现这一想法的关键在于 `RequireRole` 的 `HasServer` 实例。
## HasServer 简述
在此之前,请允许我简要说明 `HasServer` 类。本文并非 Servant 教程,因此我会跳过许多细节。
它有一个关联类型和两个方法:
```haskell
class HasServer api context where
type ServerT api (m :: Type -> Type) :: Type
route :: Proxy api -> Context context -> Delayed env (Server api) -> Router env
hoistServerWithContext
:: Proxy api -> Proxy context -> (forall x. m x -> n x) -> ServerT api m -> ServerT api n
type Server api = ServerT api Handler
```
`api` 是 Servant 组合子,描述 API 结构的一部分。`HasServer` 实例是 API 描述与实际路由处理器之间的桥梁。
关联类型 `ServerT` 告诉编译器如何将 `api` 类型转换为处理器类型签名的片段。
例如,`Verb` 的 `ServerT` 关联类型为:
```haskell
type ServerT (Verb method status ctypes a) m = m a
```
这意味着 `Verb 'GET 200 '[JSON] a` 映射到处理器签名中的 `m a`。
`route` 构建一个称为 `Router` 的分发树,Servant 随后通过 `serve` 将其转换为 WAI Application 以处理请求。
每个 API 组件都有自己的 `route` 定义,它们递归地构建一个 `Delayed` 计算,用于生成处理器的输入。
例如,`Capture "id" Int` 表示获取下一个 URL 路径段,尝试将其解析为 `Int`,然后传递给处理器。将更多 API 组件串联起来,就构建出 `Delayed` 计算,其结果会传递给处理器函数。
最后是 `hoistServerWithContext`。Servant 应用通常用自定义单子 `m` 编写,但最终需要在 `Handler` 中运行。我们使用自然变换将 `m` 映射到 `Handler`。该函数说明了如何通过这个 API 组件传播自然变换。
## 我们的实例
我们的数据类型将包含一个符号,表示在 `Context` 中查找的认证方法,以及一个角色 `r`,用于检查已认证用户的角色:
```haskell
data RequireRole (tag :: Symbol) (r :: k)
```
`hoistServerWithContext` 的定义很平凡,只是将自然变换传递给下一个 API 组件。
`route` 则是我们完成所有工作的地方。我们需要从 `AuthHandler` 中获取 `AuthServerData`,并调用 `checkRole` 来比较用户角色与 API 组件中要求的角色。
为此,我们需要创建另一个类型类,告诉如何从我们的认证上下文中提取角色。
```haskell
class HasRole auth r | auth -> r where
getRole :: auth -> r
instance HasRole Authz UserRole where
getRole = userRole
```
然后我们用关联类型和 `Proxy` 来完善 `CheckRole`:
```haskell
class CheckRole (r :: k) where
type RoleType r :: Type
checkRole :: Proxy r -> RoleType r -> Bool
```
现在在 `route` 内部,我们可以使用 `Proxy` 将 `CheckRole` 特化为实例 `r`,并针对 `getRole` 得到的用户角色调用 `checkRole`:
```haskell
checkRole (Proxy @r) (getRole auth)
```
如果角色检查失败,我们抛出一个 403 错误。否则,允许 `Delayed` 计算继续携带 `AuthServerData`。
我们通过 `delayedFail` 触发失败。这会使错误非致命,允许 Servant 尝试下一个 `:<|>` 候选项。这为我们提供了匹配相同路由路径但不同角色要求时的回退行为。
实际的认证查找失败会调用 `delayedFailFatal`,立即返回。这意味着我们拒绝所有未认证的请求。
我们也可以在此处使用 `delayedFail`,允许未认证的请求通过每一道关卡后再失败。这让我们可以创建一个未认证的回退路由。
这是一个设计选择,也许我应该提供两种行为的组合子?
完整的 `HasServer` 实例:
```haskell
instance
forall tag r api context.
( HasServer api context,
CheckRole r,
HasRole (AuthServerData (AuthProtect tag)) (RoleType r),
HasContextEntry context (AuthHandler Request (AuthServerData (AuthProtect tag)))
) =>
HasServer (RequireRole tag r :> api) context
where
type
ServerT (RequireRole tag r :> api) m =
AuthServerData (AuthProtect tag) -> ServerT api m
hoistServerWithContext _ pc nt s =
hoistServerWithContext (Proxy @api) pc nt . s
route _ context subserver =
route (Proxy @api) context (subserver `addAuthCheck` withRequest authCheck)
where
authHandler' :: Request -> Handler (AuthServerData (AuthProtect tag))
authHandler' = unAuthHandler (getContextEntry context)
authCheck :: Request -> DelayedIO (AuthServerData (AuthProtect tag))
authCheck req = do
eResult <- liftIO $ runHandler (authHandler' req)
case eResult of
Left err -> delayedFailFatal err
Right auth ->
if checkRole (Proxy @r) (getRole auth)
then pure auth
else
delayedFail
err403
{ errBody = "Forbidden: insufficient permissions",
errHeaders = [("Content-Type", "text/plain; charset=utf-8")]
}
```
有了一个可工作的 servant 组合子,我们就可以构建一个可工作的示例。
```haskell
data UserRole = Viewer | Editor | Admin
deriving (Ord)
instance CheckRole 'Viewer where
type RoleType 'Viewer = UserRole
checkRole _ role = role >= Viewer
instance CheckRole 'Editor where
type RoleType 'Editor = UserRole
checkRole _ role = role >= Editor
instance CheckRole 'Admin where
type RoleType 'Admin = UserRole
checkRole _ role = role >= Admin
data Authz = Authz { userRole :: UserRole, userName :: String }
deriving (Show)
instance HasRole Authz UserRole where
getRole = userRole
type instance AuthServerData (AuthProtect "test-auth") = Authz
type PanelAdminAPI =
RequireRole "test-auth" 'Admin
:> "panel"
:> Get '[JSON] String
type PanelEditorAPI =
RequireRole "test-auth" 'Editor
:> "panel"
:> Get '[JSON] String
type PanelViewerAPI =
RequireRole "test-auth" 'Viewer
:> "panel"
:> Get '[JSON] String
type API = PanelAdminAPI :<|> PanelEditorAPI :<|> PanelViewerAPI
server :: Server API
server = panelAdmin :<|> panelEditor :<|> panelViewer
where
panelAdmin :: Authz -> Handler String
panelAdmin _ = pure "admin panel"
panelEditor :: Authz -> Handler String
panelEditor _ = pure "editor panel"
panelViewer :: Authz -> Handler String
panelViewer _ = pure "viewer panel"
```
不错!
这已经相当简洁,但我觉得还能更好。我们按照用户角色限制了处理器的访问权限,但我们的处理器仍然可以调用任何子例程。
如果在角色检查期间构造一个特殊的 `Proof` 令牌,我们就可以限制处理器能调用的子例程。
这个 `Proof` 令牌由 `HasServer` 的 `route` 函数中检查的认证角色索引。然后我们可以构建像这样的函数:
```haskell
banUser :: Proof 'Admin -> Authz -> String
banUser _proof auth = "banned by " <> userName auth
```
而且我们只能从 `'Admin` 认证作用域的处理器中调用这个函数。
注意,因为 `Authz` 本身尚未(!)由角色索引,所以我们并没有证明某个**特定的**用户通过了角色检查,只证明了**某个**用户通过了。
要使其工作,我们需要定义几个数据类型:
```haskell
data Proof (required :: k) = Proof
data Satisfies (required :: k) authz = Satisfies (Proof required) authz
```
`Proof` 是某个角色满足需求 `required` 的见证。构造函数不导出,因此构造它的唯一方式是通过新的函数 `checkAuth`,它在 `authCheck` 中被调用,如果 `checkRole` 成功则产生一个 `Proof`。
`Satisfies` 是一个认证结果,并带有一个证明它满足 `required` 的见证。这就是处理器接收到的内容。
`checkAuth` 替换了 `authCheck` 中的 `if` 语句,并产生我们的 `Proof`:
```haskell
checkAuth :: CheckRole required => Proxy required -> RoleType required -> Maybe (Proof required)
checkAuth p role
| checkRole p role = Just Proof
| otherwise = Nothing
```
`authCheck` 现在返回 `Satisfies required (AuthServerData (AuthProtect tag))`:
```haskell
authCheck :: Request -> DelayedIO (Satisfies required (AuthServerData (AuthProtect tag)))
authCheck request = do
eResult <- liftIO $ runHandler (authHandler' request)
case eResult of
Left err -> delayedFailFatal err
Right auth ->
case checkAuth (Proxy @required) (getRole auth) of
Just proof -> pure $ Satisfies proof auth
Nothing ->
delayedFail
err403
{ errBody = "Forbidden: insufficient permissions",
errHeaders = [("Content-Type", "text/plain; charset=utf-8")]
}
```
现在我们的处理器接收 `Satisfies required (AuthServerData (AuthProtect tag))`,允许管理员处理器使用证明来调用 `banUser`:
```haskell
adminHandler :: Satisfies 'Admin Authz -> Handler String
adminHandler (Satisfies proof auth) = pure (banUser proof auth)
```
其他处理器不能调用 `banUser`,因为它们拥有错误的证明,这体现在它们的 `Satisfies` 参数上:
```haskell
editorHandler :: Satisfies 'Editor Authz -> Handler String
editorHandler (Satisfies _proof auth) = pure $ "editor: " <> show (userName auth)
viewerHandler :: Satisfies 'Viewer Authz -> Handler String
viewerHandler (Satisfies _proof auth) = pure $ "viewer: " <> show (userName auth)
```
我们已经将子例程限制为具有适当角色检查的处理器。但我们还没有将这些子例程限制为**那些**通过了角色检查的用户。在 `editorHandler` 内部,我们可以获取其他用户的 `Authz`,并使用我们获得的 `Proof 'Admin`。
要防止这种情况,我们需要将 `UserRole` 从 `Authz` 内部的值提升为 `UserRole` 上的索引:
```haskell
newtype Authz (r :: UserRole) = Authz {userName :: String}
```
换言之,目前证明与主体是独立的。我们证明了**某个人**是管理员(或其它),但没有证据表明是谁。
事实证明,这需要进入所谓的 hasochism (https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf) 领域。
## (别怕)收割者
剩下的部分会有些残酷。我将介绍一个基于 singletons 的最小化解决方案,没有所有花里胡哨的特性,并带有大量样板代码。在实际的 `servant-auth-roles` 库中,我采用了一个略有不同的 singletons 方法,并通过 Template Haskell 隐藏所有内容以消除样板代码。
## 具体化与伪造
singletons 的基本概念是我们构造一个 GADT,它唯一地映射到索引类型的索引。这允许你通过模式匹配 GADT 在运行时恢复类型层面的信息。
```haskell
data SBool (b :: Bool) where
STrue :: SBool 'True
SFalse :: SBool 'False
```
使用 `SBool`,GADT 的每个分支都将 `b` 特化为 `Bool` kind 的一个类型。这意味着当模式匹配时,GHC 能够根据分支推断出 `b`。
这允许我们执行具体化,即从值映射到类型。
想象一下尝试编写这个函数:
```haskell
toSBool :: Bool -> SBool b
```
无论你返回 `SBool` 的哪种情况,都会得到类型错误,因为 `b` 是普遍量化的。然而,如果我们将参数隐藏在存在量词后面,那么我们可以编写:
```haskell
data SomeSBool where
SomeSBool :: SBool b -> SomeSBool
toSBool :: Bool -> SomeSBool
toSBool True = SomeSBool STrue
toSBool False = SomeSBool SFalse
```
现在,当我们模式匹配 `SomeBool` 时,我们可以访问特化的 `b`。这允许我们编写像这样的函数:
```haskell
fireTheMissiles :: SBool 'True -> IO ()
fireTheMissiles STrue = print "Missiles have been fired!"
check :: Bool -> IO ()
check input = case toSBool input of
SomeSBool tru -> fireTheMissiles tru
SomeSBool SFalse -> pure ()
```
用 `SFalse` 调用 `fireTheMissiles` 会导致类型错误,因为它要求 `SBool 'True`。这就是我们想玩的把戏的味道。然而,此时我们可以在 `SFalse` 分支中伪造一个 `STrue`:
```haskell
SomeSBool SFalse -> fireTheMissiles STrue
```
为了防止伪造,我们需要引入一个证据类型,它与索引 `b` 共享。这样我们就可以强制我们的 `SBool` 与证据的 `SBool` 匹配。
```haskell
data IsTrue (b :: Bool) where
IsTrue :: IsTrue 'True
decide :: SBool b -> Maybe (IsTrue b)
decide STrue = Just IsTrue
decide SFalse = Nothing
fireTheMissiles :: IsTrue b -> SBool b -> IO ()
fireTheMissiles = ...
```
调用 `fireTheMissiles` 的唯一方式是确保我们的 `SBool b` 与我们的 `IsTrue b` 匹配:
```haskell
check :: Bool -> IO ()
check input = case toSBool input of
SomeSBool sb -> case decide sb of
Just ev -> fireTheMissiles ev sb
Nothing -> pure ()
```
现在,我们只能在 `input` 为 `True` 的情况下调用 `fireTheMissiles`,并且我们通过 `decide` 产生了 `input` 为 `True` 的证据。
让我们看看我们的 `banUs`...
相似文章
可验证的智能体基础设施:面向主权AI系统的基于证明的授权机制
本文提出了一种分布式信任框架(DTF),用于自主AI代理系统中的可验证、基于证明的授权,通过要求提供理由证明和共识执行来应对以身份为中心的权限所带来的风险。
提示注入即角色混淆
本文提出一种理论,认为对大型语言模型的提示注入攻击源于模型在角色感知上的根本缺陷——将角色视为语言的类型系统。该理论解释了现有攻击,预测了新型攻击,并提出了关于角色科学的研究议程。
物理AI中的静默故障:自主系统运行时动作授权文献综述
本文献综述识别并分析了物理AI系统中静默故障的问题,即黑箱模型可能在未被检测到的情况下执行有害动作。它提出了运行时防护功能分类法,并概述了安全自主系统的评估要求。
面向特定领域智能体的符号护栏:不牺牲实用性的更强安全与保障
本文提出符号护栏,通过具体策略为特定领域AI智能体提供可证明的安全与保障,同时不降低实用性;实验显示74%的指定策略可通过简单机制强制执行。
多智能体人工智能系统中的授权传播:将身份治理作为基础设施
本文引入了“授权传播”这一多智能体人工智能系统中独特的安全挑战,并提出必须将身份治理视为基础设施,以在自主智能体交互中维持授权不变量。