{-# LANGUAGE DeriveDataTypeable #-}
-- |
-- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier
-- License : GPL v3 (see LICENSE)
--
-- Maintainer : Simon Meier <iridcode@gmail.com>
-- Portability : GHC only
--
-- Main module for the tamarin prover.
module Main where
import Prelude hiding (id, (.))
import Data.List
import Data.Maybe
import Data.Version (showVersion)
import Data.Monoid
import Data.Char (isSpace, toLower)
import Data.Label
import Control.Basics
import Control.Category
import Control.Exception as E
import System.Console.CmdArgs.Explicit
import System.Console.CmdArgs.Text
import System.Exit
import System.FilePath
import System.Directory
import System.Environment
import System.IO
import System.Process
import System.Timing (timed)
import Extension.Prelude
import qualified Text.Isar as Isar
import Theory
import Theory.Parser
import Theory.Wellformedness
import Paths_tamarin_prover
import Web.Dispatch
import qualified Web.Settings
import qualified Network.Wai.Handler.Warp as Warp (run)
------------------------------------------------------------------------------
-- General definitions for tamarin
------------------------------------------------------------------------------
-- | Program name
programName :: String
programName = "tamarin-prover"
-- | Version string
versionStr :: FilePath -- ^ Path to LICENCE file.
-> String
versionStr licensePath = unlines
[ concat
[ programName
, " "
, showVersion version
, ", (C) Benedikt Schmidt, Simon Meier, ETH Zurich 2010-2012"
]
, ""
, "This program comes with ABSOLUTELY NO WARRANTY. It is free software, and you"
, "are welcome to redistribute it according to its LICENSE, see"
, "'" ++ licensePath ++ "'."
]
-- | Line width to use.
lineWidth :: Int
lineWidth = 110
shortLineWidth :: Int
shortLineWidth = 78
{-
-- | Version string with HTML markup.
htmlVersionStr :: String
htmlVersionStr = concat
[ link "http://www.infsec.ethz.ch/research/software#TAMARIN" programName
, " "
, showVersion version
, ", © "
, link "https://infsec.ethz.ch/infsec/people/benschmi/index" "Benedikt Schmidt"
, ", "
, link "http://people.inf.ethz.ch/meiersi" "Simon Meier"
, ", ETH Zurich 2010-2012"
]
where
link href name =
"<a href=\"" ++ href ++ "\" target=\"new\">" ++ name ++ "</a>"
-}
------------------------------------------------------------------------------
-- Argument parsing helpers
------------------------------------------------------------------------------
type Arguments = [(String,String)]
argExists :: String -> Arguments -> Bool
argExists a = isJust . findArg a
findArg :: MonadPlus m => String -> Arguments -> m String
findArg a' as = msum [ return v | (a,v) <- as, a == a' ]
getArg :: String -> Arguments -> String
getArg a =
fromMaybe (error $ "getArg: argument '" ++ a ++ "' not found") . findArg a
addArg :: String -> String -> Arguments -> Arguments
addArg a v = ((a,v):)
withArguments :: Mode Arguments -> (Arguments -> IO ()) -> IO ()
withArguments argMode io = do
licensePath <- getDataFileName "LICENSE"
processArgs argMode >>= run licensePath
where
run licensePath as
| argExists "help" as = print $ helpText HelpFormatAll argMode
| argExists "version" as = putStrLn $ versionStr licensePath
| otherwise = io as
updateArg :: String -> String -> Arguments -> Either a Arguments
updateArg a v = Right . addArg a v
addEmptyArg :: String -> Arguments -> Arguments
addEmptyArg a = addArg a ""
-- | Main mode.
mainMode :: Mode [(String,String)]
mainMode =
-- translateMode { modeGroupModes = toGroup [interactiveMode] }
translateMode { modeGroupModes = toGroup [interactiveMode, intruderMode] }
where
defaultMode name help = Mode
{ modeGroupModes = toGroup []
, modeNames = [name]
, modeValue = []
, modeCheck = updateArg "mode" name
, modeReform = const Nothing-- no reform possibility
, modeHelp = help
, modeHelpSuffix = []
, modeArgs = Nothing -- no positional arguments
, modeGroupFlags = toGroup [] -- no flags
}
translateMode =
( defaultMode programName
"Batch mode for analyzing security protocols using DH-exponentiation."
)
{ modeCheck = updateArg "mode" "translate"
, modeArgs = Just $ flagArg (updateArg "inFile") "FILES"
, modeGroupFlags = Group
{ groupUnnamed =
theoryLoadFlags ++
-- [ flagNone ["html"] (addEmptyArg "html")
-- "generate HTML visualization of proofs"
-- [ flagNone ["no-compress"] (addEmptyArg "noCompress")
-- "Do not use compressed sequent visualization"
[ flagNone ["parse-only"] (addEmptyArg "parseOnly")
"Parse the input file and pretty-print it as-is"
] ++
outputFlags ++
toolFlags
, groupHidden = []
, groupNamed =
[ ("About"
, [ flagHelpSimple (addEmptyArg "help")
, flagVersion (addEmptyArg "version")
] )
]
}
}
intruderMode =
( defaultMode "intruder"
"Compute the variants of the intruder rules for DH-exponentiation."
)
{ modeArgs = Nothing
, modeCheck = updateArg "mode" "intruder"
, modeGroupFlags = toGroup outputFlags
}
outputFlags =
[ flagOpt "" ["output","o"] (updateArg "outFile") "FILE" "Output file"
, flagOpt "" ["Output","O"] (updateArg "outDir") "DIR" "Output directory"
]
toolFlags =
-- [ flagOpt "dot" ["with-dot"] (updateArg "withDot") "FILE" "Path to GraphViz 'dot' tool"
[ flagOpt "maude" ["with-maude"] (updateArg "withMaude") "FILE" "Path to 'maude' rewriting tool"
]
interactiveFlags =
[ flagOpt "" ["port","p"] (updateArg "port") "PORT" "Port to listen on"
-- , flagOpt "" ["datadir"] (updateArg "datadir") "DATADIR" "Directory with data"
, flagNone ["debug"] (addEmptyArg "debug") "Show server debugging output"
-- , flagNone ["autosave"] (addEmptyArg "autosave") "Automatically save proof state"
-- , flagNone ["loadstate"] (addEmptyArg "loadstate") "Load proof state if present"
] ++
theoryLoadFlags ++
toolFlags
interactiveMode =
( defaultMode "interactive"
"Start a web-server for interactively constructing the security proofs."
)
{ modeArgs = Just $ flagArg (updateArg "workDir") "WORKDIR"
, modeCheck = updateArg "mode" "interactive"
, modeGroupFlags = toGroup interactiveFlags
}
-- | Disply help message and exit.
errHelpExit :: String -> IO ()
errHelpExit msg = do
putStrLn $ "error: " ++ msg
putStrLn $ ""
putStrLn $ showText (Wrap lineWidth)
$ helpText HelpFormatDefault mainMode
examplePath <- getDataFileName "examples"
let userGuidePath = examplePath </> "UserGuide.spthy"
csf12Path = examplePath </> "csf12" </> "*.spthy"
csf12Cmd = programName ++ " --prove -Ocase-studies +RTS -N -RTS " ++ csf12Path
csf12Cmd' = programName ++ " interactive +RTS -N -RTS " ++ csf12Path
separator = putStrLn $ replicate shortLineWidth '-'
putPath info path = putStrLn info >> putStrLn (" " ++ path ++ "\n")
separator
putPath "For example protocol models see" examplePath
putPath "Their syntax is explained in" userGuidePath
putPath "To run all case-studies from our CSF'12 submission, use" csf12Cmd
putPath "To construct their security proofs interactively, use" csf12Cmd'
putStrLn
"Note that the +RTS -N -RTS flags instruct the Haskell runtime system to\n\
\use as many cores as your system has. This speeds-up some of the computations."
separator
exitFailure
where
------------------------------------------------------------------------------
-- Main mode execution
------------------------------------------------------------------------------
-- | Main function.
main :: IO ()
main =
withArguments mainMode selectMode
where
selectMode as = case findArg "mode" as of
Just "translate" -> translate as
Just "intruder" -> intruderVariants as
Just "interactive" -> interactive as
Just m -> error $ "main: unknown mode '" ++ m ++ "'"
Nothing -> error $ "main: no mode given"
-- shared support functions
---------------------------
renderDoc :: Isar.Doc -> String
renderDoc = Isar.renderStyle (Isar.style { Isar.lineLength = lineWidth })
------------------------------------------------------------------------------
-- Intruder variants mode execution
------------------------------------------------------------------------------
intruderVariants :: Arguments -> IO ()
intruderVariants as = do
ensureMaude as
hnd <- startMaude (maudePath as) dhMaudeSig
let thy = dhIntruderTheory hnd
thyString = renderDoc $ prettyOpenTheory thy
putStrLn thyString
writeThy thyString
where
-- output generation
--------------------
writeThy thyString = case optOutPath of
Just outPath -> writeFileWithDirs outPath thyString
Nothing -> return ()
-- Output file name, if output is desired.
optOutPath :: Maybe FilePath
optOutPath =
do outFile <- findArg "outFile" as
guard (outFile /= "")
return outFile
<|>
do outDir <- findArg "outDir" as
return $ outDir </> defaultIntrVariantsPath
defaultIntrVariantsPath :: FilePath
defaultIntrVariantsPath = "intruder_variants_dh.spthy"
------------------------------------------------------------------------------
-- Theory loading: shared between interactive and batch mode
------------------------------------------------------------------------------
theoryLoadFlags :: [Flag Arguments]
theoryLoadFlags =
[ flagNone ["prove"] (addEmptyArg "addProofs")
"Attempt to prove all security properties"
, flagOpt "dfs" ["stop-on-attack"] (updateArg "stopOnAttack") "DFS|BFS|NONE"
"How to search for attacks (default DFS)"
-- , flagOpt "5" ["bound", "b"] (updateArg "bound") "INT"
-- "Bound the depth of the proofs"
--, flagOpt "" ["intruder","i"] (updateArg "intruderVariants") "FILE"
-- "Cached intruder rules to use"
, flagOpt "" ["defines","D"] (updateArg "defines") "STRING"
"Define flags for pseudo-preprocessor."
]
loadOpenThy :: Arguments -> FilePath -> IO OpenTheory
loadOpenThy = fst . loadThy
loadClosedThy :: Arguments -> FilePath -> IO ClosedTheory
loadClosedThy = uncurry (>=>) . loadThy
loadClosedWfThy :: Arguments -> FilePath -> IO ClosedTheory
loadClosedWfThy as file = do
thy <- loadOpen file
case checkWellformedness thy of
[] -> close thy
report -> error $ renderDoc $ prettyWfErrorReport report
where
(loadOpen, close) = loadThy as
loadClosedThyString :: Arguments -> String -> IO ClosedTheory
loadClosedThyString = uncurry (>=>) . loadThyString
-- | Load an open/closed theory from a file.
loadThy :: Arguments -> (FilePath -> IO OpenTheory, OpenTheory -> IO ClosedTheory)
loadThy as = loadGenericThy (parseOpenTheory (defines as)) as
-- | Load an open/closed theory from a string.
loadThyString :: Arguments -> (String -> IO OpenTheory, OpenTheory -> IO ClosedTheory)
loadThyString as = loadGenericThy loader as
where
loader str =
case parseOpenTheoryString (defines as) str of
Right thy -> return thy
Left err -> error $ show err
-- | The defined pre-processor flags in the argument.
defines :: Arguments -> [String]
defines = findArg "defines"
-- | Load an open/closed theory given a loader function.
loadGenericThy :: (a -> IO OpenTheory)
-> Arguments
-> (a -> IO OpenTheory, OpenTheory -> IO ClosedTheory)
loadGenericThy loader as =
(loader, (closeThy as) <=< tryAddIntrVariants)
where
-- intruder variants
--------------------
tryAddIntrVariants :: OpenTheory -> IO OpenTheory
tryAddIntrVariants thy0 = do
let msig = get (sigpMaudeSig . thySignature) thy0
thy = addIntrRuleACs (subtermIntruderRules msig ++ specialIntruderRules) thy0
if (enableDH msig) then
do variantsFile <- getDataFileName "intruder_variants_dh.spthy"
ifM (doesFileExist variantsFile)
(do intrVariants <-
get thyCache <$> parseOpenTheory (defines as) variantsFile
return $ addIntrRuleACs intrVariants thy
)
(error $ "could not find intruder message deduction theory '"
++ variantsFile ++ "'")
else return thy
-- | Close a theory according to arguments.
closeThy :: Arguments -> OpenTheory -> IO ClosedTheory
closeThy as =
fmap (proveTheory prover) . closeTheory (maudePath as) . wfCheck
where
-- handles to relevant arguments
--------------------------------
proofBound = read <$> findArg "bound" as
requireProofs = argExists "addProofs" as
stopOnAttack :: Maybe String
stopOnAttack = findArg "stopOnAttack" as
-- wellformedness check
-----------------------
wfCheck :: OpenTheory -> OpenTheory
wfCheck thy =
noteWellformedness
(checkWellformedness thy) thy
-- protocol transformation
--------------------------
prover :: Prover
prover
| requireProofs = cutAttack $ maybe id boundProver proofBound autoProver
| otherwise = mempty
where
cutAttack = mapProverProof $ case map toLower <$> stopOnAttack of
Nothing -> cutOnAttackDFS
Just "dfs" -> cutOnAttackDFS
Just "none" -> id
Just "bfs" -> cutOnAttackBFS
Just other -> error $ "unknown stop-on-attack method: " ++ other
------------------------------------------------------------------------------
-- Tool paths (shared between interactive and batch mode)
------------------------------------------------------------------------------
-- | Path to maude tool
maudePath :: Arguments -> FilePath
maudePath = fromMaybe "maude" . findArg "withMaude"
-- | Path to dot tool
dotPath :: Arguments -> FilePath
dotPath = fromMaybe "dot" . findArg "withDot"
------------------------------------------------------------------------------
-- Interactive proof mode execution
------------------------------------------------------------------------------
-- | Prove lemmas interactively.
interactive :: Arguments -> IO ()
interactive as = case findArg "workDir" as of
Nothing -> errHelpExit "no working directory specified"
Just workDir0 -> do
-- determine working directory
wdIsFile <- doesFileExist workDir0
let workDir | wdIsFile = takeDirectory workDir0
| otherwise = workDir0
wdIsDir <- doesDirectoryExist workDir
if wdIsDir
then do
-- process theories
ensureGraphVizDot as
ensureMaude as
putStrLn ""
port <- readPort
dataDir <- readDataDir
putStrLn $ intercalate "\n"
[ "The server is starting up on localhost with port " ++ show port ++ "."
, "Browse to http://localhost:" ++ show port ++ " once the server is ready."
, ""
, "Loading the security protocol theories '" ++ workDir </> "*.spthy" ++ "' ..."
]
withWebUI workDir (argExists "loadstate" as) (argExists "autosave" as)
(loadClosedWfThy as) (loadClosedThyString as) (closeThy as)
(argExists "debug" as) (Just dataDir) (Warp.run port)
else errHelpExit $ "directory '" ++ workDir ++ "' does not exist."
where
-- Datadir argument
readDataDir =
case findArg "datadir" as of
[d] -> return d
_ -> getDataDir
-- Port argument
----------------
readPort = do
let port = findArg "port" as >>= fmap fst . listToMaybe . reads
when
(argExists "port" as && isNothing port)
(putStrLn $ "Unable to read port from argument `"
++fromMaybe "" (findArg "port" as)++"'. Using default.")
return $ fromMaybe Web.Settings.defaultPort port
------------------------------------------------------------------------------
-- Translate mode execution
------------------------------------------------------------------------------
-- | Execute a translation.
translate :: Arguments -> IO ()
translate as
| null inFiles = errHelpExit "no input files given"
| otherwise = do
ensureMaude as
putStrLn $ ""
summaries <- mapM processThy inFiles
putStrLn $ ""
putStrLn $ replicate shortLineWidth '='
putStrLn $ "summary of processed files:"
putStrLn $ ""
putStrLn $ renderDoc $ Isar.vcat $ intersperse (Isar.text "") summaries
putStrLn $ ""
putStrLn $ replicate shortLineWidth '='
where
-- handles to arguments
-----------------------
inFiles = reverse $ findArg "inFile" as
-- output generation
--------------------
dryRun = not (argExists "outFile" as || argExists "outDir" as)
mkOutPath :: FilePath -- ^ Input file name.
-> FilePath -- ^ Output file name.
mkOutPath inFile =
fromMaybe (error "please specify an output file or directory") $
do outFile <- findArg "outFile" as
guard (outFile /= "")
return outFile
<|>
do outDir <- findArg "outDir" as
return $ mkAutoPath outDir (takeBaseName inFile)
-- automatically generate the filename for output
mkAutoPath :: FilePath -> String -> FilePath
mkAutoPath dir baseName
| argExists "html" as = dir </> baseName
| otherwise = dir </> addExtension (baseName ++ "_analyzed") "spthy"
-- theory processing functions
------------------------------
processThy :: FilePath -> IO (Isar.Doc)
processThy inFile
-- | argExists "html" as =
-- generateHtml inFile =<< loadClosedThy as inFile
| argExists "parseOnly" as =
out (const Isar.emptyDoc) prettyOpenTheory (loadOpenThy as inFile)
| otherwise =
out prettyClosedSummary prettyClosedTheory (loadClosedThy as inFile)
where
out :: (a -> Isar.Doc) -> (a -> Isar.Doc) -> IO a -> IO Isar.Doc
out summaryDoc fullDoc load = do
res <- try $
if dryRun
then do writeWithSummary putStrLn "<no file written>"
else do
putStrLn $ ""
putStrLn $ "analyzing: " ++ inFile
putStrLn $ ""
let outFile = mkOutPath inFile
summary <- writeWithSummary (writeFileWithDirs outFile) outFile
putStrLn $ replicate shortLineWidth '-'
putStrLn $ renderDoc summary
putStrLn $ ""
putStrLn $ replicate shortLineWidth '-'
return summary
case res of
Right x -> return x
Left x -> return $ Isar.vcat $ map Isar.text
[ "failed to analyze: " ++ inFile
, ""
, " exception: " ++ show (x :: IOException)
]
where
writeWithSummary :: (String -> IO ()) -> FilePath -> IO Isar.Doc
writeWithSummary io outName = do
(thySummary, t) <- timed $ do
thy <- load
io $ renderDoc $ fullDoc thy
return $ summaryDoc thy
return $ Isar.vcat
[ Isar.text $ "analyzed: " ++ inFile
, Isar.text $ ""
, Isar.text $ " output: " ++ outName
, Isar.text $ " processing time: " ++ show t
, Isar.text $ ""
, Isar.nest 2 thySummary
]
{- TO BE REACTIVATED once infrastructure from interactive mode can be used
-- static html generation
-------------------------
generateHtml :: FilePath -- ^ Input file
-> ClosedTheory -- ^ Theory to pretty print
-> IO ()
generateHtml inFile thy = do
cmdLine <- getCommandLine
time <- getCurrentTime
cpu <- getCpuModel
template <- getHtmlTemplate
theoryToHtml $ GenerationInput {
giHeader = "Generated by " ++ htmlVersionStr
, giTime = time
, giSystem = cpu
, giInputFile = inFile
, giTemplate = template
, giOutDir = mkOutPath inFile
, giTheory = thy
, giCmdLine = cmdLine
, giCompress = not $ argExists "noCompress" as
}
-}
------------------------------------------------------------------------------
-- Utility functions
------------------------------------------------------------------------------
-- | Write a file and ensure that its containing directory exists.
writeFileWithDirs :: FilePath -> String -> IO ()
writeFileWithDirs file output = do
createDirectoryIfMissing True (takeDirectory file)
writeFile file output
-- | Get the string constituting the command line.
getCommandLine :: IO String
getCommandLine = do
arguments <- getArgs
return . concat . intersperse " " $ programName : arguments
-- | Read the cpu info using a call to cat /proc/cpuinfo
getCpuModel :: IO String
getCpuModel =
handle handler $ do
(_, info, _) <- readProcessWithExitCode "cat" ["/proc/cpuinfo"] []
return $ maybe errMsg
(("Linux running on an "++) . drop 2 . dropWhile (/=':'))
(find (isPrefixOf "model name") $ lines info)
where
errMsg = "could not extract CPU model"
handler :: IOException -> IO String
handler _ = return errMsg
-- | Get the path to the Html template file.
getHtmlTemplate :: IO FilePath
getHtmlTemplate = getDataFileName "HTML_TEMPLATE"
-- | Build the command line corresponding to a program arguments tuple.
commandLine :: String -> [String] -> String
commandLine prog args = concat $ intersperse " " $ prog : args
-- | Test if a process is executable and check its response. This is used to
-- determine the versions and capabilities of tools that we depend on.
testProcess :: (String -> String -> Either String String)
-- ^ Analysis of stdout, stderr. Use 'Left' to report error.
-> String -- ^ Test description to display.
-> FilePath -- ^ Process to start
-> [String] -- ^ Arguments
-> String -- ^ Stdin
-> IO Bool -- ^ True, if test was successful
testProcess check testName prog args inp = do
putStr testName
hFlush stdout
handle handler $ do
(exitCode, out, err) <- readProcessWithExitCode prog args inp
let errMsg reason = do
putStrLn reason
putStrLn $ " command: " ++ commandLine prog args
putStrLn $ " stdin: " ++ inp
putStrLn $ " stdout: " ++ out
putStrLn $ " stderr: " ++ err
return False
case exitCode of
ExitFailure code -> errMsg $ "failed with exit code " ++ show code
ExitSuccess ->
case check out err of
Left msg -> errMsg msg
Right msg -> do putStrLn msg
return True
where
handler :: IOException -> IO Bool
handler _ = do putStrLn "caught exception while executing:"
putStrLn $ commandLine prog args
putStrLn $ "with input: " ++ inp
return False
-- | Ensure a suitable version of the Graphviz dot tool is installed.
ensureGraphVizDot :: Arguments -> IO ()
ensureGraphVizDot as = do
putStrLn $ "GraphViz tool: '" ++ dot ++ "'"
success <- testProcess check " checking version: " dot ["-V"] ""
unless success $ putStrLn errMsg
where
dot = dotPath as
check _ err
| "graphviz" `isInfixOf` map toLower err = Right $ init err ++ ". OK."
| otherwise = Left $ errMsg
errMsg = unlines
[ "WARNING:"
, ""
, " The dot tool seems not to be provided by Graphviz."
, " Graph generation might not work."
, " Please download an official version from:"
, " http://www.graphviz.org/"
]
-- | Ensure a suitable version of Maude is installed.
ensureMaude :: Arguments -> IO ()
ensureMaude as = do
putStrLn $ "maude tool: '" ++ maude ++ "'"
success <- testProcess check " checking version: " maude ["--version"] ""
unless success $ putStrLn $ errMsg "tool not found / does not work"
where
maude = maudePath as
check out _
| filter (not . isSpace) out == "2.6" = Right "2.6. OK."
| otherwise = Left $ errMsg $
" 'maude --version' returned wrong verison '" ++ out ++ "'"
errMsg reason = unlines
[ "WARNING:"
, ""
, reason
, " " ++ programName ++ " will likely not work."
, " Please download 'Core Maude 2.6' from:"
, " http://maude.cs.uiuc.edu/download/"
]