Programming and Logic, past and futureMenu Menu
Keeping secrets are very small part of security. System must keep working high availability correctly working System may fail (ex. hardware failure, fire) Backup is important Accessibility Unusable system is the most safe one? compromise ( such as 4 digit password) Human factor Technology itself does not make the system reliable be a reliable person
Risks varies ... light or serious rare or frequent predictable or unpredictable Reliablities are relative to specifications predections
Security vs Usability Security vs Costs
Keep working? Working safely? It is available? It works even in an extreme condition?
Finite automaton ( looping on fix amount of state, very simple) CPU Memory NetworkSoftware
Operating system Application Services Framework Library Database
Program is written in programming languages Program do something depends on inputs, environment or non-determinism Program have to keep requirements
Mathematical relations of inputs and outupts These are written in logics
Logic describes relations of properties. At first, these are written in a natural language such as English or Japanese.
Philosophers (such as Euclid) separate assumptions and consequences. Theorems (Consequences) are inferred from Axioms (assumptions).
Frege deines theory of descriptions as a formal language which is not a natural languages. It contains predicate and connectives.
Value: name of some concrete things Variable: name assuming contains some value Predicate: pair of predicate name and arguments, which may true or fale Connectives: negation(not), disjunction(or), conjunction(and) Qunatifier: ∀ for all , ∃ exists
rule of manipulating symbols, which is a seriales of characters Term rewriting system (lambda calculus)
syntax definition rewriting rule
a,b,c constant x,y,z variable a constant is a term λ x -> X is a term if we have a term X f a function f and it's an argument a
( λ x -> f x ) a ----------------------- f a
x contains somethingx is a some kind of things
f xf does not accepts all possible things, but it accepts some kind of thing such as an element of Set A. f returns some kind of things such as an element of Set B.
f : A -> Bb is an element of B
b : B
assuming b : B.
f : A -> B f = λ ( x : A ) -> bassuming a : A , type of f a is B.
lemma1 : B lemma1 = f a
if P then Q (¬ P ) ∨ Q every time P is happen, Q will be true □ ( P → ◇ Q )
Specification in logic Implement in functions Execution result is set
p p is true ¬ p p is not true p ∧ q p and q is true p ∨ q p or q is true p → q p implies q ( ¬ p ∨ q )formula and it's meanings.
value of variables assert all assertions are correct (valid) in any permutated executions
□p always p ◇p sometimes p ◇p = ¬ □ ¬ p
Implemenation → SpecificationIf ¬ (Implemenation → Specification ) is satisfiable, there is a bug.
→ Model checking (SPIN / Java Pathfinder )Or we can prove ( Implemenation → Specification ) directory
→ Proof assistance ( Agda )
Proofs in a first order logic is an function ( lambda calculus)
Write down the proofs as a function
Logic formula is a type. Proof is a lambda function.
type-name : type type-name = proof as a lambda term
Interaction with outside or environments handling very large implementation and spefication in logics
Continuation based C (CbC) ( more primitve C language ) Implement Operating system on CbC Provide model checking and proof system for CbC