Survey on Runtime Monitoring based on Formal SpecificationSoftware ProgramsSafe Programs ??Safe ProgramsProgram DevelopmentProgram Safety TechniquesOutlineRuntime MonitoringSlide 9Slide 10Temporal Assertions using AspectJ (SB’05)SB’05 LanguageLTLSlide 14SB’05 Spec Evaluating ProcessAFASlide 17Slide 18Translation: LTL  AFASlide 20SB’05 Evaluation SummarySlide 22AspectJSlide 24Overall Architecture – InstrumentationSlide 26EAGLEEagle LanguageSyntaxMetric Temporal Logic (MTL)Eagle Spec Evaluation ProcessEagle Evaluation SummaryEagle Instrumentation/FeedbackSlide 34Edit AutomataEnforcing Policy in Edit AutomataSlide 37Example: Atomicity3 Works on Edit AutomataPolicy CalculusPolymerPolymer InstrumentationSlide 43Intrusion Detection using EAGLEDoS AttackSummaryLanguageSpec Evaluation ProcessWhy Checking LTL is ≈ O(2m)Why Eagle general checking time depends on length of traceOther Runtime MonitoringConclusionReferenceQ & AQ: Eagle Toward CFLQ: Eagle Regular ExpressionQ: Eagle m-CalculusQ: LTL  AFA ExampleQ: Eagle Eval ExampleQ: Eagle Eval Example (continue..)Q: Eagle Execution Time – Depending on Trace LengthQ: OverheadQ: Multithreaded and Distributed MonitoringQ: Actual Eagle LTL Checking TimeQ:Survey on Runtime Monitoringbased on Formal SpecificationWPE-II PresentationByUsa SammapunOct 28, 2005Software ProgramsHeart DeviceCarAircraftATMSafe Programs ??Safe ProgramsVerificationSecurityProgram Developmentclass AIBO { Leg leg1,leg2,leg3,leg4; main() { leg1 = new Leg(1); leg2 = new Leg(2); leg3 = new Leg(3); leg4 = new Leg(4); } }class Leg { void walk() { } void stop() { }} all-leg-down!walkleg1-up, leg4-upwalk & !fallleg2-up, leg3-upwalk & !fallleg1-up, leg2-upwalk & fallwalk and not fallRequirementModelImplementationProgram Safety TechniquesImplementationModelModel CheckingModel Carrying CodeRuntime MonitoringRequirementGoal: Ensuring that implementation satisfies requirementModel Carrying CodeOutlineOverview of runtime monitoringRuntime VerificationTemporal Assertions using AspectJ [Stolz,Bodden05]Eagle [Barringer et al. 04]SecurityEdit Automata [Bauer et al. 03]Eagle for Intrusion Detection [Naldurg et al. 2004]DiscussionConclusionRuntime MonitoringProgramsInstrumentationMonitorTrace ExtractionFeedbackFormal Specificationclass AIBO { Leg leg1,leg2,leg3,leg4; main() { leg1 = new Leg(1); send(checker,leg1); leg2 = new Leg(2); send(checker,leg2); leg3 = new Leg(3); send(checker,leg3); leg4 = new Leg(4); send(checker,leg4); } }class Leg { void walk() { send(checker,walk); } void stop() { send(checker,stop); }} leg1 leg2 leg3 leg4SatisfiedNot SatisfiedRuntime MonitoringFormal specification languageBased on MathematicsLogics, Automata, CalculiInstrumentationManual & Automatic Bytecode & SourcecodeSpecification Evaluation ProcessTransform spec language into a checking automatonTakes a trace as an inputReturns result: Satisfied, Not SatisfiedDirect algorithmTakes both spec language and a trace as inputsReturns result: Satisfied, Not SatisfiedFeedbackOptionalFixed or user-definedOutlineOverview of runtime monitoringRuntime VerificationTemporal Assertions using AspectJ [Stolz,Bodden05]Eagle [Barringer et al. 04]SecurityEdit Automata [Bauer et al. 03]Eagle for Intrusion Detection [Naldurg et al. 2004]Comparison and AnalysisConclusionTemporal Assertions using AspectJ (SB’05)Specification Language: LTLSpec Evaluation Process: Alternating AutomataInstrumentation: Automatic: AspectJBytecodeFeedback: AspectJSB’05 LanguageLTL – Linear Temporal LogicReason about time-dependent truth valueClassical: 1 < 2 Temporal: it’s rainingSyntaxf :: = p | ¬ f | f1 ∧ f2 | f1 ν f2 | ○ f | ◊ f | □ f | f1 U f2 | f1 R f2 Next Eventually Always UntilPropositionReleaseLTLfff f f f f ff1f1f1f1f2○f -- Next ◊ f -- Eventually  f ν ○(◊f)□ f – Always (Global)  f ∧ ○(□f)f1 U f2 -- Until  f2 ν (f1 ∧ ○(f1 U f2))f2f2f2f2f1f1 R f2 -- Release  f2 ∧ (f1 ν ○(f1 R f2))f2f2f2f2f2f2LTL◊ f = true U f□ f = false R fConcise Syntaxf :: = p | ¬ f | f1 ∧ f2 | f1 ν f2 | X f | f1 U f2 | f1 R f2 true true true true ff f f f f ff f f f falseSB’05 Spec Evaluating ProcessTranslate LTL formulae to Alternating AutomataUse Alternating Automata to check a traceAlternating Finite Automata (AFA)Generalization of Non-deterministic Finite Automata (NFA)NFA – existential automaton -automatonA combination of bothAFAs1s2s3s4s5s6s7s8s9s10On input a : T(s1, a) = {s2, s5, s8, s9} NFA: Accept - automata: RejectAFA: Dependss1s2s3s4s9s8s5AFA = (, S, s0, T, F)The only difference from NFA is the transition functionTNFA(s1, a) = {s2, s5, s8, s9} = s2 ν s5 ν s8 ν s9TAFA(s1,a) = (s2 ν s5) ∧ (s8 ν s9) Choose to go to {s5, s9}, then acceptTAFA(s1,a) = s2 ∧ (s5 ν s8 ν s9) Reject, no matter what you chooseaaaAFAFormally, AFA = (, S, s0, T, F)T: S x   B+(S)B+(S) is a set of positive Boolean formulae over SPositive Boolean Formulae: Boolean formulae built from elements in S using ∧ and νWe say a set S’ satisfies a positive Boolean formula f in B+(S) if the truth assignment assigns true to S’ and false to S-S’For example, the set S’ = {s5, s9} satisfies the formula f = (s2 ν s5) ∧ (s8 ν s9)the set S’ = {s2, s5} does not satisfy fAFAA run r’ of NFA is linear because you only choose one pathA run r of AFA is a treeFor disjunction, you choose one pathFor conjunction, you have to take all pathsA run r of AFA on a finite word w = a1, a2, …, an is a finite tree such that if s is a node in the tree r and T(s, ai) = f, where f is positive Boolean formula then s has k children for some k ≤ |S|, and {s1, s2, …, sk} satisfies fTransition therefore determines what are possible next statesTAFA(s1,a) = (s2 ν s5) ∧ (s8 ν s9)Possible states are {s2,s8}, {s2, s9}, {s5,s8}, {s5,s9}E.g., you can’t go to state {s2,s5}AFA accepts a run r if all leaves of a run r are final statess1s5 s9Translation: LTL  AFATranslating an LTL formula f to an AFA AfAf accepts, then f satisfiesAf rejects, then f doesn’t satisfyAf= (, S, s0, T, F)