commit 4921ff38f9e774b90501559ba42ed121ee15133f
parent d6cebeeb19325432dc131a5cfede78dc89a2ae43
Author: Jared Tobin <jared@jtobin.io>
Date: Tue, 10 Feb 2026 12:26:49 +0400
fix: parser and taint analysis bugs
Parser fixes:
- Add try for register parsers to allow backtracking (sp vs s0)
- Fix pre-index addressing mode (! after ] not inside)
- Restructure line parsing to avoid infinite loop on empty lines
- Use hspace instead of space1 to preserve newlines
Taint analysis fix:
- Correct join lattice: Public+Unknown -> Unknown (not Public)
- This ensures secret-derived values are properly flagged
Tests pass. Fixtures validate correctly:
- good.s: 0 violations (10 memory accesses)
- bad.s: 4 violations detected
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Diffstat:
9 files changed, 154 insertions(+), 64 deletions(-)
diff --git a/flake.lock b/flake.lock
@@ -0,0 +1,88 @@
+{
+ "nodes": {
+ "flake-utils": {
+ "inputs": {
+ "systems": "systems"
+ },
+ "locked": {
+ "lastModified": 1731533236,
+ "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+ "type": "github"
+ },
+ "original": {
+ "owner": "numtide",
+ "repo": "flake-utils",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1766840161,
+ "narHash": "sha256-Ss/LHpJJsng8vz1Pe33RSGIWUOcqM1fjrehjUkdrWio=",
+ "owner": "NixOS",
+ "repo": "nixpkgs",
+ "rev": "3edc4a30ed3903fdf6f90c837f961fa6b49582d1",
+ "type": "github"
+ },
+ "original": {
+ "owner": "NixOS",
+ "ref": "nixpkgs-unstable",
+ "repo": "nixpkgs",
+ "type": "github"
+ }
+ },
+ "ppad-nixpkgs": {
+ "inputs": {
+ "flake-utils": "flake-utils",
+ "nixpkgs": "nixpkgs"
+ },
+ "locked": {
+ "lastModified": 1766932084,
+ "narHash": "sha256-GvVsbTfW+B7IQ9K/QP2xcXJAm1lhBin1jYZWNjOzT+o=",
+ "ref": "master",
+ "rev": "353e61763b959b960a55321a85423501e3e9ed7a",
+ "revCount": 2,
+ "type": "git",
+ "url": "git://git.ppad.tech/nixpkgs.git"
+ },
+ "original": {
+ "ref": "master",
+ "type": "git",
+ "url": "git://git.ppad.tech/nixpkgs.git"
+ }
+ },
+ "root": {
+ "inputs": {
+ "flake-utils": [
+ "ppad-nixpkgs",
+ "flake-utils"
+ ],
+ "nixpkgs": [
+ "ppad-nixpkgs",
+ "nixpkgs"
+ ],
+ "ppad-nixpkgs": "ppad-nixpkgs"
+ }
+ },
+ "systems": {
+ "locked": {
+ "lastModified": 1681028828,
+ "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+ "owner": "nix-systems",
+ "repo": "default",
+ "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nix-systems",
+ "repo": "default",
+ "type": "github"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/lib/Audit/AArch64.hs b/lib/Audit/AArch64.hs
@@ -36,6 +36,8 @@ module Audit.AArch64 (
, AuditResult(..)
, Violation(..)
, ViolationReason(..)
+ , Reg
+ , regName
-- * Re-exports
, ParseError
@@ -44,7 +46,7 @@ module Audit.AArch64 (
import Audit.AArch64.CFG
import Audit.AArch64.Check
import Audit.AArch64.Parser
-import Audit.AArch64.Types
+import Audit.AArch64.Types (Reg, Violation(..), ViolationReason(..), regName)
import qualified Data.ByteString as BS
import Data.Text (Text)
import qualified Data.Text as T
diff --git a/lib/Audit/AArch64/Check.hs b/lib/Audit/AArch64/Check.hs
@@ -23,7 +23,6 @@ import Audit.AArch64.CFG
import Audit.AArch64.Taint
import Audit.AArch64.Types
import Data.Text (Text)
-import qualified Data.Text as T
-- | Result of auditing assembly.
data AuditResult = AuditResult
diff --git a/lib/Audit/AArch64/Parser.hs b/lib/Audit/AArch64/Parser.hs
@@ -16,11 +16,11 @@ module Audit.AArch64.Parser (
import Audit.AArch64.Types
import Control.Monad (void)
-import Data.Char (isAlphaNum, isDigit, isSpace)
+import Data.Char (isAlphaNum)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Void (Void)
-import Text.Megaparsec
+import Text.Megaparsec hiding (ParseError)
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
@@ -31,10 +31,10 @@ type ParseError = ParseErrorBundle Text Void
parseAsm :: Text -> Either ParseError [Line]
parseAsm = parse (many pLine <* eof) "<asm>"
--- Space consumer (skips whitespace and comments).
+-- Space consumer (skips horizontal whitespace and comments, not newlines).
sc :: Parser ()
sc = L.space
- space1
+ hspace1
(L.skipLineComment "//")
(L.skipBlockComment "/*" "*/")
@@ -42,26 +42,23 @@ sc = L.space
lexeme :: Parser a -> Parser a
lexeme = L.lexeme sc
--- Symbol (alphanumeric + underscore + dot + dollar).
-symbol :: Text -> Parser Text
-symbol = L.symbol sc
-
-- Parse a single line.
pLine :: Parser Line
pLine = do
pos <- getSourcePos
let ln = unPos (sourceLine pos)
- skipMany (satisfy isSpace)
+ hspace -- Skip leading horizontal whitespace only
choice
[ pDirectiveLine ln
- , pLabelOrInstrLine ln
+ , pLabelLine ln
+ , pInstrLine ln
, pEmptyLine ln
]
pEmptyLine :: Int -> Parser Line
pEmptyLine ln = do
void (optional pComment)
- void (optional eol)
+ void eol -- Must consume actual newline
pure (Line ln Nothing Nothing)
pComment :: Parser ()
@@ -76,15 +73,23 @@ pDirectiveLine ln = do
void (optional eol)
pure (Line ln Nothing Nothing)
-pLabelOrInstrLine :: Int -> Parser Line
-pLabelOrInstrLine ln = do
- mLabel <- optional (try pLabel)
- skipMany (satisfy isSpace)
+pLabelLine :: Int -> Parser Line
+pLabelLine ln = do
+ lbl <- try pLabel
+ hspace
mInstr <- optional pInstr
- skipMany (satisfy isSpace)
+ hspace
+ void (optional pComment)
+ void (optional eol)
+ pure (Line ln (Just lbl) mInstr)
+
+pInstrLine :: Int -> Parser Line
+pInstrLine ln = do
+ instr <- pInstr
+ hspace
void (optional pComment)
void (optional eol)
- pure (Line ln mLabel mInstr)
+ pure (Line ln Nothing (Just instr))
pLabel :: Parser Text
pLabel = lexeme $ do
@@ -242,7 +247,7 @@ pComma = void (lexeme (char ','))
pReg :: Parser Reg
pReg = lexeme $ choice
- [ pXReg, pWReg, pDReg, pSReg, pQReg, pSpecialReg ]
+ [ try pXReg, try pWReg, try pDReg, try pSReg, try pQReg, pSpecialReg ]
pXReg :: Parser Reg
pXReg = do
@@ -377,10 +382,10 @@ pShiftAmt = do
pSymbolRef :: Parser Text
pSymbolRef = lexeme $ do
-- Handle =literal, @PAGE, @PAGEOFF suffixes, etc.
- prefix <- optional (char '=')
+ hasPrefix <- option False (True <$ char '=')
name <- pIdentifier
suffix <- optional pSymbolSuffix
- let base = maybe name (T.cons '=') prefix <> name
+ let base = if hasPrefix then T.cons '=' name else name
pure (maybe base (base <>) suffix)
pSymbolSuffix :: Parser Text
@@ -407,39 +412,34 @@ pBracketAddr = lexeme $ do
sc
base <- pReg
sc
- mode <- optional (pComma *> pAddrModeRest base)
+ innerMode <- optional (pComma *> pAddrModeInner)
sc
void (char ']')
- -- Check for pre/post index
+ -- Check for pre-index ! or post-index offset
+ preIdx <- option False (True <$ char '!')
postIdx <- optional pPostIndex
- case (mode, postIdx) of
- (Nothing, Nothing) -> pure (BaseImm base 0)
- (Nothing, Just imm) -> pure (PostIndex base imm)
- (Just (Left imm, True), Nothing) -> pure (PreIndex base imm)
- (Just (Left imm, False), Nothing) -> pure (BaseImm base imm)
- (Just (Right (r, Nothing), _), Nothing) -> pure (BaseReg base r)
- (Just (Right (r, Just (Left sh)), _), Nothing) -> pure (BaseRegShift base r sh)
- (Just (Right (r, Just (Right ext)), _), Nothing) -> pure (BaseRegExtend base r ext)
+ case (innerMode, preIdx, postIdx) of
+ (Nothing, False, Nothing) -> pure (BaseImm base 0)
+ (Nothing, False, Just imm) -> pure (PostIndex base imm)
+ (Just (Left imm), True, Nothing) -> pure (PreIndex base imm)
+ (Just (Left imm), False, Nothing) -> pure (BaseImm base imm)
+ (Just (Right (r, Nothing)), False, Nothing) -> pure (BaseReg base r)
+ (Just (Right (r, Just (Left sh))), False, Nothing) -> pure (BaseRegShift base r sh)
+ (Just (Right (r, Just (Right ext))), False, Nothing) -> pure (BaseRegExtend base r ext)
_ -> fail "invalid addressing mode"
-pAddrModeRest :: Reg -> Parser (Either Integer (Reg, Maybe (Either Shift Extend)), Bool)
-pAddrModeRest _ = do
- choice
- [ try pImmOffset
- , pRegOffset
- ]
-
-pImmOffset :: Parser (Either Integer (Reg, Maybe (Either Shift Extend)), Bool)
-pImmOffset = do
- imm <- pImm
- preIdx <- optional (char '!')
- pure (Left imm, maybe False (const True) preIdx)
+-- Parse the inner part of [base, ...] after the comma
+pAddrModeInner :: Parser (Either Integer (Reg, Maybe (Either Shift Extend)))
+pAddrModeInner = choice
+ [ Left <$> pImm
+ , Right <$> pRegWithModifier
+ ]
-pRegOffset :: Parser (Either Integer (Reg, Maybe (Either Shift Extend)), Bool)
-pRegOffset = do
+pRegWithModifier :: Parser (Reg, Maybe (Either Shift Extend))
+pRegWithModifier = do
r <- pReg
modifier <- optional (pComma *> pShiftOrExtend)
- pure (Right (r, modifier), False)
+ pure (r, modifier)
pShiftOrExtend :: Parser (Either Shift Extend)
pShiftOrExtend = choice
diff --git a/lib/Audit/AArch64/Taint.hs b/lib/Audit/AArch64/Taint.hs
@@ -80,7 +80,7 @@ transfer instr st = case instr of
-- Move: destination gets source taint
Mov dst op -> setTaint dst (operandTaint op st) st
Movz dst _ _ -> setTaint dst Public st -- Immediate is public
- Movk dst _ _ -> st -- Keeps existing value, modifies bits
+ Movk _ _ _ -> st -- Keeps existing value, modifies bits
Movn dst _ _ -> setTaint dst Public st -- Immediate is public
-- Arithmetic: result is join of operand taints
diff --git a/lib/Audit/AArch64/Types.hs b/lib/Audit/AArch64/Types.hs
@@ -225,13 +225,13 @@ data Taint
instance ToJSON Taint
-- | Join operation for taint lattice (least upper bound).
--- Unknown < Public < Secret
+-- For CT safety: Public only if both are Public.
+-- Order: Public < Unknown < Secret
joinTaint :: Taint -> Taint -> Taint
-joinTaint Secret _ = Secret
-joinTaint _ Secret = Secret
-joinTaint Public _ = Public
-joinTaint _ Public = Public
-joinTaint Unknown Unknown = Unknown
+joinTaint Public Public = Public
+joinTaint Secret _ = Secret
+joinTaint _ Secret = Secret
+joinTaint _ _ = Unknown -- Public+Unknown or Unknown+Unknown
-- | Reason for a violation.
data ViolationReason
diff --git a/ppad-auditor.cabal b/ppad-auditor.cabal
@@ -45,7 +45,8 @@ executable auditor
ghc-options:
-Wall -O2 -threaded
build-depends:
- base
+ aeson
+ , base
, bytestring
, optparse-applicative >= 0.16 && < 0.19
, ppad-auditor
diff --git a/test/Main.hs b/test/Main.hs
@@ -97,7 +97,7 @@ taintTests = testGroup "Taint" [
-- X0 = X20 (public) + X1 (unknown) -> unknown
l = Line 1 Nothing (Just (Add X0 X20 (OpReg X1)))
st' = analyzeLine l st
- assertEqual "result is public" Public (getTaint X0 st')
+ assertEqual "result is unknown" Unknown (getTaint X0 st')
, testCase "load makes unknown" $ do
let st = initTaintState
diff --git a/test/fixtures/bad.s b/test/fixtures/bad.s
@@ -11,20 +11,20 @@ _unsafe_function:
mov x29, sp
; Load a secret value
- ldr x0, [x20] ; x0 = secret from memory
+ ldr x0, [x20]
- ; BAD: Use secret as base address (cache-timing leak)
- ldr x1, [x0] ; violation: unknown base x0
+ ; BAD: Use secret as base address
+ ldr x1, [x0]
- ; BAD: Use secret as index (cache-timing leak)
- ldr x2, [x21, x0] ; violation: unknown index x0
+ ; BAD: Use secret as index
+ ldr x2, [x21, x0]
; BAD: Secret-derived address via arithmetic
- add x3, x0, #256 ; x3 = secret + offset
- ldr x4, [x3] ; violation: unknown base x3
+ add x3, x0, #256
+ ldr x4, [x3]
; BAD: Secret used in shifted index
- ldr x5, [x21, x0, lsl #3] ; violation: unknown index x0
+ ldr x5, [x21, x0, lsl #3]
; Frame teardown
ldp x29, x30, [sp], #16
