2015-12-13

pCICについて

TSG Advent Calendar 2015 - Adventarの12/13の記事です。

序文 - pCICとは

pCICはPredicative Calculus of (Co)Inductive Constructionsのことで、coqの型システムのことです。
定理証明支援系と言われるcoqですが、そもそもcoqで「証明する」とはどういうことでしょうか。
coqにおける命題は型(type)に、その証明は項(term)に対応しています(Curry-Howard同型を思い出してください)。つまり、coqである命題Pを証明するということは、型Pを持つ項を探してくることに対応しています。
このことから、coqの動作を理解する上でpCICを理解することは重要だと考えられます。
この記事はcoqの本質とも言えるpCICの側面からcoqの動作について理解しようという趣旨で書かれています。自分が探した限り、そのような記事はあまりなさそうなので書くことにしました。

命題はtypeに、証明はtermに

例として

forall (P Q : Prop), P -> Q -> P.

という簡単な命題を考えてみます。

まず

Definition K : forall (P Q : Prop), P -> Q -> P.

と書くと、Kは型だけ定義されて項は定義されていない状態になります。
proof editing modeで

Show Proof.

とすると今の証明の状態が表示されるので、最初の状態なら

?1

と表示されるでしょう。?1はplaceholderで、まだ定義されていない項を表しています。
もう少し進んで

intros.
Show Proof.

としてみると

(fun (P Q : Prop) (H : P) (H0 : Q) => ?5)

と表示されます。

  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   P

?5というplaceholderは今のゴールに対応していて、P, Q, H, H0という変数を使って型Pを持つ項を作って?5の位置に入れれば証明が完成することが分かります。Hは既に型Pを持っているので、assumptionで?5にHを入れて証明は完了です。
この作業を通して、型 forall (P Q : Prop), P -> Q -> P を持つ項を定義し、それにKという名前をつけました。

Print K.

でそれを確認できます。
証明とは言っても、ある型を持つ項を定義するだけなので、最初から項を与えてしまっても同じことです。それを確認するためにK'を定義しました。
先ほどplaceholderがゴールに対応していると言いましたが、複数のゴールがあるときは複数のplaceholderがあるときです。上のコードの後半はそれを確認するための例です。

ちなみに

forall x : P, M.

という形の式でMにxが(自由に)現れない場合

P -> M

と表現されます。
つまり「ならば」を意味する"->"は実際にはforallです。

pure type system

pCICについてはChapter 4 Calculus of Inductive Constructionsに書いてあるので、これを解説すればよいのですが、やや複雑なので、先にpure type systemについて説明したいと思います。
pure type systemは型付きラムダ計算のフレームワークの一つで、適当なパラメーターを設定すれば単純型付きラムダ計算や多相型、依存型を含んだ型付きラムダ計算の体系なども作ることができます。pCICもベースはこのpure type systemなので(たぶん)、最初にpure type systemを簡単に理解しておくとpCICもスムーズに理解できるかと思います。
pure type systemについてはpure type system in nLabとかLectures on the Curry-Howard Isomorphismとかを見ると良いと思います。
pure type systemは $(S, A, R)$ の三つ組をパラメーターとして与えることで定まります。termとtypeは構文的には同じで、constant, variable, abstruction, product, applicationによって、再帰的に定義されます。
$T := c | x | \lambda x : T . T | \Pi x : T . T | T T$
このconstantを与えるのが $S$ (sort)です。また、 $\lambda, \Pi$ は変数を束縛します。
そして、このtermを用いてtype judgement $\vdash$ を定義します。この定義についてはnlabを参照してください。 $A$ は(axioms)に、 $R$ は(product)に使われています。
$\Gamma \vdash M : t$ の $\Gamma$ はcontextと呼ばれることが多いです。これは変数宣言のリストと考えてください。慣れている人にはわざわざ説明する必要はないと思いますが、 $\vdash$ という記号は大抵「 $\vdash$ の左を仮定した時に $\vdash$ の右が導ける」という意味で使われ、今回使う $x_1 : t_1, \dots, x_n : t_n \vdash M : t$ も「変数 $x_1$ が型 $t_1$ , .. , 変数 $x_n$ が型 $t_n$ であると仮定した時に、項 $M$ は型 $t$ である」と考えてください。
$\Gamma$ は順序も重要なので気をつけてください。

pCIC

ここからChapter 4 Calculus of Inductive Constructionsの内容に入っていきます。

Term

pure type systemのtermに let .. in .. を付け足したくらいしか差はありません。
coqではabstruction: $\lambda x : t. M$ は fun x: t => M に、product: $\Pi x : t. M$ は forall x:t, M に対応します。

Context

上で説明したpure type systemと少し変わるところは、context $\Gamma$ はglobal environment $E$ とlocal context $\Gamma$ に分けられ、 $E [ \Gamma ]$ と表されます。また、 $E [ \Gamma ]$ の中には変数の型の宣言 $x : t$ だけではなく、変数の定義 $x:=M : t$ も認められます。

Local context

最初の例で説明すると

  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   P

における、横棒の上のやつのことです。
pure type systemでのcontextとほぼ同じですが、上で書いたように変数の定義も認められています。

Goal let n := 1 in n = 1.
intro.

  n := 1 : nat
  ============================
   n = 1

Environment

coqのリファレンスマニュアルには

An environment is an ordered list of declarations of global names. Declarations are either assumptions or “standard” definitions, that is abbreviations for well-formed terms but also definitions of inductive objects.

とあります。
Assumptionにはこの辺のtacticsが対応してます。ここに書いてあるのは実質AxiomとVariableの2つだけで、違いはVariableの方はSectionの中に閉じ込められることです。
Definitionにはこの辺のtacticsが対応してます。先ほどと同じように、DefinitionとLetがあって、LetはSectionの中に閉じ込められます。
Environmentを見るにはPrint Allというコマンドを使えば良さそうです。
次の例を試してみると動作がよく解ると思います。

bとdがSectionの外では見えなくなること、bとdを使って定義されたeがSectionの外ではどうなるのかということに注意してください。
EnvironmentにはInductiveの定義も含まれるようです。

Typing rules

だいたいpure type systemと同じなので三つ組 $(S, A, R)$ を与えるだけにとどめます。
$S = \{{\tt Prop}, {\tt Set}, {\tt Type}(i) | i \in \mathbb{N}\}$
$A = \{({\tt Prop}, {\tt Type}(i)) | i \in \mathbb{N}\} \cup \{({\tt Set}, {\tt Type}(i)) | i \in \mathbb{N}\} \cup \{({\tt Type}(i), {\tt Type}(j)) | i< j\}$
$R = \{(s, {\tt Prop}) | s \in S\} \cup \{({\tt Prop}, {\tt Set}), ({\tt Set}, {\tt Set})\} \cup \{({\tt Type}(i), {\tt Type}(j), {\tt Type}(k)) | i, j \le k\}$
ここで、 $(s1, s2) \in R$ は $(s1, s2, s2) \in R$ という意味であることに気をつけてください。

Conversion rules

pure type systemでは簡約はβ簡約だけでしたが、pCICではいくつかあります。そのため、pure type systemよりも(conversion)規則は複雑です。

β-reduction

通常のβ簡約

ι-reduction

inductive objectに関する簡約らしいです。

δ-reduction

$E$ や $\Gamma$ に変数の定義( $x:=M : t$ )が含まれるとき、項の中の $x$ を $M$ で置き換えることです。

ζ-reduction

δ-reductionと似ていますが、
${\tt let}\; x:=M \; {\tt in} \; N$ を $N\{x:=M\}$ とする簡約です。

η-conversion

$M$ と $\lambda x : t . M x$ ( $x$ は $M$ の自由変数に含まれない)を同一視することです。

最後に

実はまだInductive Definitions以降はちゃんと読んでいないのでInductiveについてはよくわかっていません。Inductiveについてはそのうち書こうかなと思っています。
pure type systemについてももう少し詳しく説明するべきだった気もするので気が向いたら書きます。

2015-12-06

CPU実験について(完動までのまとめ)

CPU実験 Advent Calendar 2015 - Adventarの記事です。

特別面白そうな話題は思いつかなかったのでこれまでの経緯をまとめただけです。

アーキテクチャについて

まずは今回自分が作成したコアについて簡単に説明しておく。

tomasuloのアルゴリズムを使ったアウトオブオーダー実行
汎用レジスタ32bit×32個(うち一つはゼロレジスタ)
外部との入出力はRS232C
命令メモリはBlockRAM、データはSRAM
ハードウェア実装のプログラムローダー

ソースコードはここ
cpu2015g6/core · GitHub

完動までの流れ

7月末 Sセメスターのハードウェア実験の最後の課題(アキュムレータマシンを作る)で、アキュムレータマシンでは面白くなさそうなのでtomasuloの実装をする。再帰fibくらいまでは動いたが、コードが汚く論理合成にとても時間がかかる(2,3時間位)のでそれ以上続ける気が無くなった。CPU実験ではまた最初から書き直そうと思った。

9/29 班決め
10/4 ISA(暫定版)が決まる(後に何度か修正された)。コアの設計を始める。

これから使う型の定義を書くところから始め、実装を進めていく。

10/14-18 用事があったため進捗なし
10/19 Check Syntaxでinternal errorが発生する。最初のxstクソ案件。
10/20 internal errorの原因はだいたいわかったが、論理合成はまだできない。
10/22,23 論理合成に成功したが、LUTを128%も使っていた。レジスタの数を減らすことで大きく改善されることが分かった。
10/28 xstがよくわからないerrorを吐くが原因がわからない。xstクソ案件。
10/31 ネストしたrecordが原因だったらしい。xstクソ案件解決。
11/3 modelsimと実機の動作が一致しない。
11/5 behavioralとpost-translateの2種類のシミュレーションを行ったところ既に動作が一致しない。xstクソ案件。

度重なるxstクソ案件でつらい時期

11/9 とある列挙型が何故か壊れることが原因だと判明した。xstクソ案件解決。
11/9 コンパイラがほぼ完成し、シミュレーターではmin-rtが動く状態になる。
11/10 最初の命令が実行されないバグを見つけて修正した。
11/11,12 再帰fibが一度動いたが、プログラムローダーを実装したらまた動かなくなった。プログラムローダーでいろいろ試したところ、SRAMの挙動が怪しそうであった。
11/16 SRAMが直った。再帰fibが動いたのでそろそろmin-rtを試してみようと考える。
11/16夜他の班が完動したのに便乗して寿司を食べに行く。QOLが大いに向上する。
11/19,20 シリアル通信の動作が安定しないことに気が付いた。入力にラッチを挟んでいなかったことが原因だった。
11/20-22 min-rtを実機で動かしたところ、write_ppm_header関数の出力は確認できたが、そこで止まってしまっているようだった。printfデバッグを始める。
11/23 FPUの挙動におかしな点を見つける。FPU係に修正を依頼し、夜には実機が画像を出力した。
11/24 シミュレーター側のFPUの修正の結果diffがなくなり完動。

これまでに踏んできたバグについて

SRAMのタイミングの問題

今使っている基板のSRAMは入出力のタイミングが難しいようで、マニュアルではreadもwriteもアドレスを入力してから2クロック後にデータのやりとりを行うことになっているが、3クロック待たないと出力が出てこないように見えることがある。レイテンシは少し大きくなるがSRAMへの入出力にはラッチを挟んだほうが(たぶん)挙動は安定する。

シリアル通信のラッチ

シリアル通信(受信側)の入力を一旦ラッチに受け取らないとたまに受信したデータが壊れる。ハードウェア実験のときにはラッチを入れなくても何故か動いてしまったのでCPU実験まで気が付かなかった。

procedureの引数の型に(package).(type)の形式のものがあるとCheck Syntaxでinternal error

record型などをpackageとしてまとめていたので、それをprocedureの引数の指定に使おうと思ったら論理合成どころかCheck Syntaxでinternal errorが発生した。型名をaliasで置き換えたらinternal errorは発生しなくなったが、論理合成では別のエラーとなったので、仕方なくprocedureを諦めて直に書くことにした。
xstはクソ。

xstのよくわからないエラーで論理合成できない

発生したエラーはERROR:Xst:1706とERROR:Xst:1847。原因はネストしたrecordがxstの御機嫌を損ねたことらしかった。ネストの深いところにあったとあるメンバを浅いところに移動させたところ何故かエラーが出なくなった。
このエラーについてgoogle検索しても使えそうな文書が見当たらず、最初は原因がさっぱり分からなかった。論理合成中にWARNING:Xst:737(このwarningはvariableの初期化を適切に行っていない時に発生することがある)が出ていることも少し経ってから見つけたが、variableの初期化漏れは全く見つからなかったのでxstのrecordの扱いがおかしいのではないかと疑い、試行錯誤の結果エラーは発生しなくなった(WARNING:Xst:737も消えた)。
また、このバグを突き止めようと試行錯誤していた時に、recordのメンバの順序を変えただけでinternal errorが発生したこともあった。
xstはクソ。

とある列挙型が(xstのバグにより)壊れる

再帰fibがmodelsimの上では動くようになったので実機で動かそうとしたところ、おかしな挙動をした。
バグが出たら最初にxstを疑うようになった私は、iseのシミュレーションの画面でbehavioral,post-translate,post-map,post-routeの4つが選べることに気が付いて、post-translateで再帰fibを動かしてみた。
post-*は論理合成後のシミュレーションを行うのでbehavioralに比べて実機に忠実なシミュレーションであり、xstのバグのせいでおかしな動作をする場合にはpost-*でも捉えられるはずである。ただbehavioralに比べて遅いし、当然論理合成してからでないとシミュレーションはできない。
post-translateでおかしな挙動を捉えることには成功したが、原因の箇所を特定する作業はとても面倒だった。post-translateではtopからの出力以外はsignalやvariableの値を確認することは難しいので、値を確認するには何らかの形でtopから出力させる必要があった。しかし、そのための書き換えを行うたびに論理合成を行う必要があり、やたらと時間がかかった。
結局、とある列挙型が何故か壊れるようだったので列挙型をやめてstd_logic_vectorとconstantの組み合わせに書きなおしたら直った。
xstはクソ。

その他

その他にもここで詳しく説明するほどではないが些細なバグがいくつかあった。

最初の命令が実行されない
プログラムローダーが終了しない
signalの初期化忘れ

など

VHDLの書き方関係

基本的な方針としては(他の言語でも同じだけど)

適当な大きさに分割して読みやすくする
同じ処理、同じ値は一箇所にまとめて容易に書き換えられるようにする

ということに気をつけてコードを書いていた。

library

std_logic_arithは使わずにnumeric_stdを使った。

twoproc

wasabizさんの記事 twoprocの書き方 - wasabizの日記参照
完全に従ってるわけではないがクロック同期な部分と組み合わせ回路を分けて書くと動作が分かりやすい。あとはprocessの中の方がforとか使えるので組み合わせ回路も書きやすい。

function, procedure

ひとまとまりの処理に名前をつける。

record

データをまとめる。
初期化に使う値はよく使うのでrecordの定義の直後にconstantとして定義しておくことが多かった。

type pohe is record
  p, o, h, e : std_logic;
end record;
constant pohe_zero : pohe := ('0', '0', '0', '0');
signal s : pohe := pohe_zero;

また、recordへの代入は

s <= (
  p => '1',
  o => '0',
  h => '1',
  e => '0'
);

のような書き方もできるので、これもよく使った。

列挙型

type pohe is (P, O, H, E);

std_logic_vectorとconstantの組み合わせでもできなくはないがこちらの方が使いやすい。
また、場合分けの時に列挙型とcaseの組み合わせで使うと(othersを使わなければ)漏れがあったときにエラーになるのでバグが減らせるかも。

constant (integer)

std_logic_vectorの幅の指定に使って、後から変更したくなった時に一箇所書き換えれば済むようにした。

知ってると便利かも

subtype

std_logic_vectorに何のデータが入っているのかを表す名前をつける目的でよく使った。

alias

signal s : std_logic_vector(31 downto 0);
alias pohe : std_logic_vector(7 downto 0) is s(31 downto 24);

とすれば

pohe <= x"41";

は

s(31 downto 24) <= x"41";

と同じである。

2015-01-20

平方根を求める回路

大学の冬休みの課題(ハードウェア構成法講義 - 平木研究室)で25bitの小数P( $1 \le P < 4$ )の平方根A(25bit)を求める回路を書くという課題が出たのでその方法を考えた。

気の向くうちにと勢いで書いた記事なので分かりにくかったり間違えてたりするかも。

問題の設定

小数の平方根も実際にやることは整数の平方根を求めることと同じなので以下では非負整数の平方根を考える。
以下では非負整数のみ考えるので整数といえば非負整数を指すことにする。

25bitという具体的な数ではかえって本質が分かりにくくなるので整数Nと置き換え、問題の設定を(少し改変して)述べると
「2Nビットの整数Pの上位Nビットが与えられる。下位Nビットは0である。また、Pは
$2^{2N-2} \le P < 2^{2N}$
を満たす。
その平方根A(Nビット)を求めよ。」
となる。

丸め処理については1ビット多めに計算することで対応できるのでここでは考えないことにして、 $A^2 \le P$ を満たす最大の整数Aを求める。

mがnビット整数であることは $0 \le m < 2^n$ と同値であり、mの下位nビットが0であることはある整数m'が存在して $m = m' 2^n$ となることと同値であることを注意しておく。

また、nビット整数Iの二進数表現の $2^k$ の位をI(k)と表記する。これはVHDLのstd_logic_vector(n-1 downto 0)を意識した表記である。例えばLSBはI(0)、MSBはI(n-1)となる。また、 $2^i$ の位から $2^j$ の位( $i>j$ )までを取り出したものをI(i..j)のように表記する。これはVHDLではI(i downto j)に対応する。

1.素朴な方法

Aの取りうる範囲に対して二分探索を行うことで平方根を求めることができる。
つまり、 $2^{N-1} \le A < 2^N$ は既に分かっていることに注意すると擬似コードは

A <- 2^(N-1)
for k in N-2..0
  if (A+2^k)^2 <= P
    A <- A+2^k

とすることでAが求まる
この方法では2乗を直接計算しているのであまり良くない

2.開平法

$(A+2^k)^2 = A^2 + 2^{k+1}A + 2^{2k}$
より、1での2乗計算は加算だけで済ませることができる(2のべき乗はシフト演算に過ぎない)
変数Qに $P-A^2$ を保存することにすると、擬似コードは

A <- 2^(N-1)
Q <- P - 2^(2*(N-1))
for k in N-2..0
  if A*2^(k+1) + 2^(2k) <= Q
    A <- A+2^k
    Q <- Q - (A*2^(k+1) + 2^(2k))

これは2進数での開平法を計算していることになる

3.開平法(改良版)

2の方法のQはそのままでは2Nビットの整数として扱うことになるが実はこの中で1が立っているビットはある範囲にかたまっていて、(ループしている間に範囲がスライドしていくが)N+2ビットで表現できる。また、Qに合わせてifの条件文やQの更新の式を書き換えると、シフト演算も1ビットシフトだけでできるようになる。

基本的には2のコードを基本にするのだが、話がややこしくなるので変数の意味とビット幅をまとめておく。

k : ループのカウンタ。n-2から0まで1ずつ減る。
P : 2Nビット。入力された整数(上位Nビット)と0(下位Nビット)。
A : Nビット。最終的にはPの平方根がここに計算される。ループのブロックの先頭では下位k+1ビット(=A(k..0))は0でループの中でA(k)が決定される。初期値は $2^{N-1}$
Q : 2Nビット。 $P - A^2$ に等しい。

このときループのブロックの先頭ではQはQ(N+k+1..k+1)の範囲だけで表現できる(つまり、ループのブロックの末尾ではQ(N+k..k)の範囲で表現される)。qをQ(N+k+1..k+1)とすると

q : N+1ビット。ループのブロックの先頭で $Q = q 2^{k+1}$ が成り立つ。

2のコードをqを用いて書き換えることで、コードが簡略化される。

また、ループのブロックの末尾では、上の条件でkを1減らしたものをそれぞれの変数が満たしている必要がある。つまり、ループ末尾で

A : 下位kビット(=A(k-1..0))は0。
Q : $P - A^2$ に等しい。
q : $Q = q 2^{k}$ を満たす。

A、Qがこの条件を満たすことは明らかなので以下ではqについて考えていく。

QがQ(N+k+1..k+1)の範囲だけで表現できること、つまりqの存在については

ループ先頭で $0 \le Q < 2^{N+N-2+2}$ かつQの下位N-2+1ビットが0
ループ末尾で $0 \le Q < 2^{N+k+1}$ かつQの下位kビットが0

を示せば良い。

最初の方は初期値についての条件だが、これを満たすことは容易に確認できる。

2つ目の方はループ末尾でのA, Qの満たす条件を用いて示す。
Aの下位kビットは0なのでA'(N-kビット整数)が存在して $A = A' 2^k$ を満たす。
$Q = P - A^2 = P - A'^2 2^{2k}$ であり、Pの下位Nビットは0、 $A'^2 2^{2k}$ の下位2kビットは0なのでQの下位 $\min \{N, 2k \}$ ビットは0である。 $0 \le k < N-2$ より $\min \{N, 2k \} \ge k$ なのでQの下位kビットは0である。
また、Aの計算方法を考えると $(A' 2^k)^2 \le P < ((A'+1) 2^k)^2$ が成り立っているので
$0 \le Q = P - (A' 2^k)^2 < (2A'+1) 2^{2k} < 2^{N-k+1} 2^{2k} = 2^{N+k+1}$
よって、 $0 \le Q < 2^{N+k+1}$ かつQの下位kビットが0が示された。

それでは2のコードをqを用いて書き換えていこう。
qの初期値はQ(2N-1..N-1)、つまり $P - 2^{2(N-1)}$ の上位N+1ビット分を取れば良い
ifの条件式 $A 2^{k+1} + 2^{2k} \le Q$ は $Q = q 2 ^ {k+1}$ より $2A + 2^k \le 2q$ と書き換える。両辺ともN+2ビットの整数として計算できる。
Qの更新は
$q 2^k \leftarrow q 2^{k+1} - (A 2^{k+1} + 2^{2k})$
と書き換えて(左辺のQは $q 2^k$ に、右辺のQは $q 2^{k+1}$ になっていることに注意)
$q \leftarrow 2q - (2A + 2^k)$
となる。ここで左辺はN+1ビットだが右辺はN+2ビットで計算したものから最上位1ビット(必ず0になる)を除いたものであることに注意する。
else文を追加しないとif文が不成立の時qが更新されないのでelseに
$q \leftarrow 2q$
も追加する。
改めて擬似コードを書くと

A <- 2^(N-1)
q <- P - 2^(2*(N-1)) の上位N+1ビット
for k in N-2..0
  if 2*A + 2^k <= 2*q
    A <- A+2^k
    q <- 2*q - (2*A + 2^k) の下位N+1ビット
  else
    q <- 2*q の下位N+1ビット

さらに、ループの中に現れるkは2^kの形しかないので、 $c = 2^k$ としてkを除くこともできる。最終的には

A <- 2^(N-1)
q <- P - 2^(2*(N-1)) の上位N+1ビット
c <- 2^(N-2)
while c > 0
  if 2*A + c <= 2*q
    A <- A + c (+ではなくorでも同じ)
    q <- 2*q - (2*A + c) の下位N+1ビット
  else
    q <- 2*q の下位N+1ビット
  c <- (c >> 1) (右に1ビットシフト)

となる。
VHDLのコンパイラがどれほど賢いのか自分はわからないので、最後のkを取り除く変形に意味があるのかは怪しいが、1ビットシフトの方が単純そうな気がする。

2014-09-30

Linux-PAM

PAMについて調べたことのまとめ。内容については十分確認してないのでもしかしたら見当違いな事を書いてるかもしれない。

PAMとは

Pluggable Authentication Module
認証処理を行うモジュール群とそれを利用するためのAPIからなるユーザー認証システム
http://www.linux-pam.org/ のドキュメントでは認証処理を行うモジュールをLinux-PAM Module、APIを利用するアプリケーションをLinux-PAM Applicationと呼んでいる

モジュールの例

Chapter 6. A reference guide for available modules

pam_unix

linuxでログインするとき/etc/passwdや/etc/shadowを見て認証を行う

pam_time

/etc/security/time.confの記述に従って、時間帯によるログインの制限ができる

pam_nologin

root以外のログインを禁止する

pam_permit

常に許可する

pam_mount

ログイン時に自動でマウントする
暗号化したホームディレクトリのマウントなどに使える

pam_ldap

ldapによる認証を行う

アプリケーションの例

sudo
login

PAMの動作

/etc/pam.d/*に各Applicationがどのようにモジュールを利用するかを記述したファイルが存在する
Linuxの各アプリケーションが共通して利用する「PAM認証」についてやhttps://www.freebsd.org/doc/en/articles/pam/pam-essentials.htmlが分かりやすい

% ls /etc/pam.d/
accountsservice                cron                          newusers
chfn                           cups-daemon                   other
chpasswd                       gnome-screensaver             passwd
chsh                           lightdm                       polkit-1
common-account                 lightdm-autologin             ppp
common-auth                    lightdm-greeter               samba
common-password                lightdm-remote-freerdp        su
common-session                 lightdm-remote-uccsconfigure  sudo
common-session-noninteractive  login
% cat /etc/pam.d/login
#
# The PAM configuration file for the Shadow `login' service
#

# Enforce a minimal delay in case of failure (in microseconds).
# (Replaces the `FAIL_DELAY' setting from login.defs)
# Note that other modules may require another minimal delay. (for example,
# to disable any delay, you should add the nodelay option to pam_unix)
auth       optional   pam_faildelay.so  delay=3000000

# Outputs an issue file prior to each login prompt (Replaces the
# ISSUE_FILE option from login.defs). Uncomment for use
# auth       required   pam_issue.so issue=/etc/issue

# Disallows root logins except on tty's listed in /etc/securetty
# (Replaces the `CONSOLE' setting from login.defs)
#
# With the default control of this module:
#   [success=ok new_authtok_reqd=ok ignore=ignore user_unknown=bad default=die]
# root will not be prompted for a password on insecure lines.
# if an invalid username is entered, a password is prompted (but login
# will eventually be rejected)
#
# You can change it to a "requisite" module if you think root may mis-type
# her login and should not be prompted for a password in that case. But
# this will leave the system as vulnerable to user enumeration attacks.
#
# You can change it to a "required" module if you think it permits to
# guess valid user names of your system (invalid user names are considered
# as possibly being root on insecure lines), but root passwords may be
# communicated over insecure lines.
auth [success=ok new_authtok_reqd=ok ignore=ignore user_unknown=bad default=die] pam_securetty.so

# Disallows other than root logins when /etc/nologin exists
# (Replaces the `NOLOGINS_FILE' option from login.defs)
auth       requisite  pam_nologin.so

# SELinux needs to be the first session rule. This ensures that any 
# lingering context has been cleared. Without out this it is possible 
# that a module could execute code in the wrong domain.
# When the module is present, "required" would be sufficient (When SELinux
# is disabled, this returns success.)
session [success=ok ignore=ignore module_unknown=ignore default=bad] pam_selinux.so close

# This module parses environment configuration file(s)
# and also allows you to use an extended config
# file /etc/security/pam_env.conf.
# 
# parsing /etc/environment needs "readenv=1"
session       required   pam_env.so readenv=1
# locale variables are also kept into /etc/default/locale in etch
# reading this file *in addition to /etc/environment* does not hurt
session       required   pam_env.so readenv=1 envfile=/etc/default/locale

# Standard Un*x authentication.
@include common-auth

# This allows certain extra groups to be granted to a user
# based on things like time of day, tty, service, and user.
# Please edit /etc/security/group.conf to fit your needs
# (Replaces the `CONSOLE_GROUPS' option in login.defs)
auth       optional   pam_group.so

# Uncomment and edit /etc/security/time.conf if you need to set
# time restrainst on logins.
# (Replaces the `PORTTIME_CHECKS_ENAB' option from login.defs
# as well as /etc/porttime)
# account    requisite  pam_time.so

# Uncomment and edit /etc/security/access.conf if you need to
# set access limits.
# (Replaces /etc/login.access file)
# account  required       pam_access.so

# Sets up user limits according to /etc/security/limits.conf
# (Replaces the use of /etc/limits in old login)
session    required   pam_limits.so

# Prints the last login info upon succesful login
# (Replaces the `LASTLOG_ENAB' option from login.defs)
session    optional   pam_lastlog.so

# Prints the message of the day upon succesful login.
# (Replaces the `MOTD_FILE' option in login.defs)
# This includes a dynamically generated part from /run/motd.dynamic
# and a static (admin-editable) part from /etc/motd.
session    optional   pam_motd.so  motd=/run/motd.dynamic noupdate
session    optional   pam_motd.so

# Prints the status of the user's mailbox upon succesful login
# (Replaces the `MAIL_CHECK_ENAB' option from login.defs). 
#
# This also defines the MAIL environment variable
# However, userdel also needs MAIL_DIR and MAIL_FILE variables
# in /etc/login.defs to make sure that removing a user 
# also removes the user's mail spool file.
# See comments in /etc/login.defs
session    optional   pam_mail.so standard

# Standard Un*x account and session
@include common-account
@include common-session
@include common-password

# SELinux needs to intervene at login time to ensure that the process
# starts in the proper default security context. Only sessions which are
# intended to run in the user's context should be run after this.
session [success=ok ignore=ignore module_unknown=ignore default=bad] pam_selinux.so open
# When the module is present, "required" would be sufficient (When SELinux
# is disabled, this returns success.)

Programming

認証の情報はpam_handle_t型(へのポインタ)のpamhが持っている
Application側もModule側もpam_set_itemやpam_get_itemで必要な情報をsetしたりgetしたりする
struct pam_convにApplicationとModuleが直接やりとりするためのcallback関数を設定する

モジュールを書く

The Linux-PAM Module Writers' Guide
コードはlinux-pam.gitのmodules(特にpam_permitは単純)やSample PAM Moduleを参考にすればいいと思う

pam_get_user: PAM_USERか、PAM_USERがNULLならプロンプトを出してユーザー名を取得する

アプリケーションを書く

The Linux-PAM Application Developers' Guide
Sample PAM Applicationやsudoのソースコードのplugins/sudoers/auth/pam.c、loginのソースコードのlogin.cが参考になると思う
sudoやloginのソースコードの取得はUbuntuなら`apt-get source sudo(またはlogin)`とすればいいはず

pam_chauthtok
authentication token(パスワードとか)の変更
pam_open_session
認証に成功したユーザーのセッションの開始時に呼び出す。pam_close_sessionをあとで呼び出すべきである。
pam_close_session
セッション終了時に呼び出す。
pam_acct_mgmt
パスワードの期限切れ、アカウントの期限切れなどを調べてユーザーアカウントが有効かどうかを判定する
It is typically called after the user has been authenticated.
pam_setcred
It should be called to set the credentials after a user has been authenticated and before a session is opened for the user (with pam_open_session(3)).
pam_authenticate
ユーザーの認証
pam_fail_delay
pam_authenticateが認証に失敗した時にアプリケーションに制御を返すまでの時間を設定する
pam_start
初期化
第一引数service_nameが/etc/pam.d/に対応する
pam_end
pam_strerror
エラーコードを説明する文字列

モジュールで実装する関数とAPIの対応

Application側API	Module側
pam_authenticate	pam_sm_authenticate
pam_setcred	pam_sm_setcred
pam_acct_mgmt	pam_sm_acct_mgmt
pam_open_session	pam_sm_open_session
pam_close_session	pam_sm_close_session
pam_chauthtok	pam_sm_chauthtok

呼び出す順序は3.4. Transactionsが詳しい

2014-07-16

netrw v147でディレクトリ名が日本語を含むとき正しく動作しない

Ubuntuにvimをインストールした時に一緒に入っていたnetrw v147ではディレクトリ名が日本語を含むとき、ディレクトリの移動ができなかったり、ファイルがちゃんと開けなかったりしたので解決法を調べてみた。

最初に見つけたのは
netrwで全角ではじまるディレクトリ名が扱えない · Issue #489 · vim-jp/issues · GitHub
これを読むとv150では直っているらしいのでhttp://www.vim.org/scripts/script.php?script_id=1075からv150をダウンロードしてインストールしてみた。

vim netrw.vba.gz
:let g:vimball_home = "/usr/share/vim/vim74"
:so %
:q

(vimballとかいうものを使っているらしい。http://nanasi.jp/articles/vim/vimball_vim.htmlも参考にした。)

インストールした後動作を確認したところ、今度はディレクトリを移動する度に

function 54_NetrwBrowseChgDir..54_NetrwOptionRestore の処理中にエラー>
が検出されました:
行 69:
E354: 無効なレジスタ名: '*'
続けるにはENTERを押すかコマンドを入力してください

というエラーが出るようになった。

この件については
https://groups.google.com/forum/#!topic/vim_dev/iEiInCavWKc
に添付されているnetrw.vba.gzを使うことで解決できた。

2014-04-09

ksnctf 23 Villager B

Villager Bを解いたのでその記録
大まかな方針だけ書くようにしますが自力で解きたい人は見ないでください

問題の確認

To be more secure I enabled several security options as follows:

Randomized addresses of the program (-pie)

Protected the stack (-fstack-protector-all)

Made GOT read-only (-Wl,-z,relro,-z,now)

Executed via xinetd

Inserted a wait in order to prevent brute force attacks

Ascii armor is enabled

pieオプションとアドレスのランダム化
-fstack-protector-allオプション(これでなにが変わるのかは知らない。カナリアとか?)
GOTがread-only(プログラムのロード時にアドレスを解決してread-onlyにするってこと?)
xinetd(inetd の仕組みを見てみる - naoyaのはてなダイアリーによるとソケットを標準入出力にdup2して、サーバーとなるプログラムをexecしてくれるものらしい)を通して実行
待ち時間(sleep)がはさんである
Ascii armor(調べたところ共有ライブラリのアドレスに0x00(ヌル文字)が含まれるようにする)が有効

とのことらしい

ディスアセンブル

プログラムvillagerをダウンロードしてobjdump -dでディスアセンブルする...がcallのオペランドがなんだかおかしい
しかしgdbでdisasコマンドをやってみたら呼び出し先の関数名がちゃんと表示された
(-pieオプションのせいか)libcの関数がPLTを経由せずに呼び出されていて、プログラムのロード時にローダーが.textセクションを直接書き換えてると考えられる
ロードする前のプログラムではアドレスが解決されていないのでcallする先が正しく表示されない

自分が知らないことが多く推測ばかりになってしまったけど、gdbでとりあえずディスアセンブルはできた

アセンブリを読む

gdbでプログラムを動かしながらmain関数とそこから呼び出されている_Z4convvという二つの関数を見てみる
ちなみに

echo '_Z4convv' | c++filt

とすると、_Z4convvはマングルされる前はconv()という名前だったと分かる
main関数は3秒sleepして_Z4convvを呼び出すことを繰り返しているがこれが "Inserted a wait in order to prevent brute force attacks" の意味だろう
mainと_Z4convvから呼び出されているlibcの関数を見てみるとputs、fflush、sleep、fgets、printfなんかが見つかる
このうちprintfは書式文字列攻撃に使える可能性がある
printfの呼び出しの周辺をみると_Z4convvで二回呼び出されているうちの二回目はfgetsの第一引数、つまり標準入力から入力された文字列が入っている配列のアドレスを直接第一引数に渡している
これで書式文字列攻撃ができることが分かった

ではどうやって攻撃するか

ここまでの流れはVillager Aと大して変わらない
問題は書式文字列攻撃をどう使うかである
"Randomized addresses of the program"によって攻撃は難しくなっている
スタックのアドレスもプログラムがロードされたアドレスもlibcのアドレスも分からないのでは攻撃できない(少なくとも自分は方法が思いつかない)
なのでアドレスを調べた
printf関数を使えばスタックの中身を表示させてスタックのアドレスと、プログラムがロードされたアドレスが分かる
libcのアドレスはputsを使ってプログラム中のlibcの関数のアドレスを含む部分(内容はAscii文字の範囲とは限らないが0x00が現れるまでは問題なくputsできるので)を送らせた
アドレスが分かれば後はlibcの適当な関数を呼び出して目的のファイルの中身を標準出力に流すだけでいい
この作業を人力でやるのは大変なのでスクリプトを書いてアドレスの計算や通信を行わせた

2014-04-09

coqのタクティックの動作

今まで何となく使っていたcoqのタクティックの動作を少し詳しく見てみることにした。

ソースコードを読むべきかもしれないけど、まずは実際どう動くかを観察して解釈することにした
以下はその記録

destruct

and(/\)のdestruct

Goal forall P Q: Prop, P/\Q -> Q/\P.
Proof.
  intros.

1 subgoal

  P : Prop
  Q : Prop
  H : P /\ Q
  ============================
   Q /\ P

ここで destruct H. を使うと仮定のP/\QがPとQになる

1 subgoal

  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   Q /\ P

Andの定義を参照すると

Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B
where "A /\ B" := (and A B) : type_scope.

さっきP/\Qをdestructして現れたPとQはconjの仮定(->の左にあるもの)であると考えられる

or(\/)のdestruct

今度は

Goal forall P Q: Prop, P\/Q -> Q\/P.
Proof.
  intros.

1 subgoal

  P : Prop
  Q : Prop
  H : P \/ Q
  ============================
   Q \/ P

仮定のP/\Qをdestructするとゴールが二つに分かれて一つ目のゴールの証明ではPが仮定、二つ目ではQが仮定となる

2 subgoals
  
  P : Prop
  Q : Prop
  H : P
  ============================
   Q \/ P

subgoal 2 is:
 Q \/ P

(一つ目のゴール証明後)

1 subgoal
  
  P : Prop
  Q : Prop
  H : Q
  ============================
   Q \/ P

orの定義を見てみると

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.

であり、二つのゴールはそれぞれのコンストラクタに対応することが分かる

代数的データ型のdestruct

では適当な代数的データ型、例えば

Inductive abc (A: Prop) (B: Prop) (C: Prop): Prop :=
c1 : A -> B -> abc A B C | c2 : C -> abc A B C.

のように定義した代数的データ型abcをdestructするとどうなるか

Goal forall A B C: Prop, abc A B C -> (A/\B) \/ C.
  intros.
  destruct H.

andとorでの結果から、このとき二つのゴールができて、一つ目のゴールではコンストラクターc1に対応してAとBを仮定に持ち、もう一つのゴールではc2に対応してCを仮定に持つようになると予想できる
そして実際そうなる

2 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  H : A
  H0 : B
  ============================
   A /\ B \/ C

subgoal 2 is:
 A /\ B \/ C

(一つ目のゴール証明後)

1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  H : C
  ============================
   A /\ B \/ C

existsのdestruct

コンストラクタにforallが含まれる場合が抜けていたことに気がついた

Goal forall (P: nat->Prop) (Q: Prop), (exists n:nat, P n) -> Q.
  intros.

1 subgoal
  
  P : nat -> Prop
  Q : Prop
  H : exists n : nat, P n
  ============================
   Q

destruct H.

1 subgoal
  
  P : nat -> Prop
  Q : Prop
  x : nat
  H : P x
  ============================
   Q

existsの定義

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
  : type_scope.

exの定義はA:=Aの部分がよく分からないが、コンストラクタex_introにforallがあるのがこれまでの例と違う

定義とdestructの動作を見比べるとex_introの中のforallのxと->の左の部分に対応するものが仮定になるようだ
これらはゴールが

forall x:A, P x -> ex (A:=A) P.

であるときにintrosで仮定に移動するものである

まとめ

destructすると代数的データ型の各コンストラクタに対応してサブゴールが作られる
そして各ゴールで仮定に追加されるものは、コンストラクタの式がゴールにあったとしてintrosタクティックで仮定に追加されるもの、である

case

destructとほとんど同じように見える
->の左に追加されるか仮定に追加されるかの違い

split

http://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic18
コンストラクタが一つの場合のみ使える
コンストラクタの中の->の左にあるものがゴールになる

面倒になってきたのでここまで