alevy/hails — comment on commit b12ace9532f0bf04de99b1275467272a90e98b9d
File: Hails/Database/MongoDB/TCB/DCAccess.hs line 127
By deian:

If you take the label:

<{["#group1" \/ "facebook"] /\ ["#group1" \/ "github"]} , {["#group1" \/ "github"] /\ ["woo"]}>

with group:

expandGroup g | g == principal "#group1" = return [principal "deian", principal "amit"]

the taintLabeled will fail, since the new label:

<{["#group1" \/ "facebook"] /\ ["amit" \/ "deian" \/ "github"]} , {["amit" \/ "deian" \/ "github"] /\ ["woo"]}>

can't be below the gitstar's clearance, which is presumably

<{["gitstar"]},True>

So instead of lines 127 and 128, we essentially want:

return $ labelTCB lbl $ unlabelTCB inp

(Though, for safety we should check that the rewritten category is still owned by p (lines 135-139)).