AURA語

CACMのType Theory Comes of Age

を丁度先週ぐらいに読みました。

話の内容としては、良く有る(のか知りませんけど)static-typingとdynamic-typingを比較してどう。
decidableとかsoundとかstrongとかsafeとかが単語としては出て来る、というのが前半。
(あんまり関係無いですが、Ruby、JavaScript、Pythonがs(ound|trong|afe)なtype systemですみたいなのは、何か違和感あるよなぁ的なソレでした。)

後半は静的型付けと動的型付けを融合(という話でFuther ReadingのHybrid Type Checking)させる試みや、Security Type SystemやRefinementなType Systemの紹介がありました。

そいでSecurity Type Systemは全然知らなかったので、丁度紹介されていたAURA語を調べて今に至るという感じです。

AURA自体は

で、F#で実装されてるぽくてこのマシンだと動かすの面倒臭いというそれだったので論文だけ読んでみました。

割とちゃんと読んだので明日の私の為に要訳を書こうと思ったのですが訳そうと思って読むとやっぱり細部が分からなかったので、理解出来た所だけメモ書きしようと思います。

メモ

Authorization Logic(日本語訳だとどうなるんだろう・・・)で仕様が定められたリクエストを対象とするようなReference Monitorを書く為のDSLぽい感じ。

Authorization Logicというのをすごく簡単に説明しようとすると...。
Reference Monitorが対象にするAuthorization Policy(これは普通に権限に関するポリシと訳せそう)が複雑になると、Monitorさんも複雑になって、Monitorさんが複雑に成るとその辺てtrusted baseなので嬉しく無い。(シンプルな方がバグさんとか困ったさんが発生しにくそうな経験則?)
そこで研究者さん達がAuthorization LogicというPrincipalやリクエスト、policy assertionに関するreasoningをやってのけちゃうヤツを作りましたみたいな。
[Authorization Logicについては、参考文献に挙げられている論文を参考にしてください...]

言語としては依存型付き言語で、ただAURAで依存型を使うのは(静的な)何かを証明するとかいうよりは、値と実行時の保証の為の証明を自然な形でくっつけて表す為に使う形になっています。

要はauthorization(権限)の表現方法で、というかlogicの言語内部への埋め込みなのですが、これはsays monadを使って実現しています。

例えば、playForという関数は

playFor : (s : Song) → (p : prin) → pf (self says MayPlay p s) → Unit

こう型付けされます。
prinというのはPrincipalの略で、Principalはまぁ人間とかシステムとか、権限の所持者みたいなものです。
MayPlayというのはassertionになっています。

これの意味する所は、このplayForを呼び出したprincipal(実行時に決まるそれは self です)がprincipal pが歌sを歌っても良いと言ってるなら歌わせるという感じです。

また

principal a
principal b
freebirdという歌がある時

ok : a says (MayPlay a freebird)

delegate : b says ((p : prin) → (s : Song) → (a says (MayPlay p s)) → (MayPlay p s))

となっている場合に b says (MayPlay a freebird) の証明は次のように書けます。

saysがmonadですから

bind delegate (λd → return b (d a freebird ok))

bindはtyping-ruleにも書いているのですが、

bind : a says P → (P → a says Q) → a says Q

です。例えばこれは

self = bとなる時に

playFor (bind delegate (λd → return b (d a freebird ok)))

とすれば歌わせる事が出来る・・・とかそういう感じになっています。

またAURAはatomicな型(principalかデータコンストラクタが引数と取らない、その意味ではenumeratedな型)同士のequalityが言えれば、convert出来る機能を実装しており、例えばこれが在ると

data Maybe (A : Set0) : Set0 where
  nothing : Maybe A
  just : A -> Maybe A

data ValTuple {A B : Set0} : A -> B -> Set0 where
  _,_ : (a : A) -> (b : B) -> ValTuple a b

data Bool : Set0 where
  true : Bool
  false : Bool

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

_==-nat_ : Nat -> Nat -> Bool
zero ==-nat zero = true
zero ==-nat (succ _) = false
(succ _) ==-nat zero = false
(succ a) ==-nat (succ b) = a ==-nat b

_==-bool_ : Bool -> Bool -> Bool
true ==-bool true = true
false ==-bool false = true
a ==-bool b = false

data List (A : Set0) : Set0 where
  [] : List A
  _::_ : A -> List A -> List A

data Obj : Set0 where
  obj : (n : Nat) -> (b : Bool) -> ValTuple n b -> Obj

getVT : (n : Nat) -> (b : Bool) -> List Obj -> Maybe (ValTuple n b)
getVT n b ((obj n' b' t) :: xs) with n ==-nat n'
... | true with b ==-bool b'
... | true = just t -- これで良い事に成る!!

この例だとNatが多分atomicな型じゃないからダメですけど...

このコードでn ==-nat n'がtrueなら、nとn'は交換可能。
同じくb ==-bool b'がtrueならbとb'は交換可能になりますよ、という感じです。

これは実行時に検査されるのですが割と柔軟で良さそうなー。(enumerated typeだけだと足りなさ気ですが。)

とかとかそういう感じに成っています。

あとは型システムのSoudness(ProgressとPreservartion)の証明とDecidabilityの証明をCoqでしましたというのがあって、1万行越えてて大変だなぁみたいな感じです・・・。

分からない点

そもそも"says"の意味する所が分からない。曰く、とか言う、とかそのまんまで訳しても大丈夫なんだろうか。

page2 : says monadがIndexed monadですと書いている所で、これがどうしてIndexed Monadになるんだろう...
page3 : なんでPropとTypeを分けているんだろう

直接は関係しないが、関連論文の"Access Control in a Core Calculus of Dependency"でQuoteが可換になっているあたり。というかPrincipalをLatticeの要素としてその上の操作と対応させて見る時のアレコレとか。