詩と創作・思索のひろば

ドキドキギュンギュンダイアリーです!!!

Fork me on GitHub

OAuth2 のフローを Alloy Analyzer でモデリングする

Alloy

趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう？ と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。

形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。

http://alloy.mit.edu/alloy/

インターネット上にチュートリアルやマニュアルもあるが、作者による教科書の邦訳が出ていて、これで勉強してみた。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

  • 作者:Daniel Jackson
  • 発売日: 2011/07/15
  • メディア: 単行本（ソフトカバー）

Halmos の握手問題

Alloy でどんな風に仕様を記述するのか、簡単な例で紹介する。ちなみにここで全ての重要な機能が解説できているわけではないので注意。

教科書の付録の練習問題として収録されているもの。

5組のカップルが参加したパーティーで、Alice が自分以外の9人に何人と握手したか尋ねると、全員から違う答えが返ってきた。自分自身と握手した人や自分のパートナーと握手した人がいないとすると、Alice のパートナー Bob は何人と握手しただろうか？

という問題。もともとは頭で解くパズルらしいけど、これを Alloy を使って解いてみる。流れとしてはこの状況を表すモデル（オブジェクトと制約）を記述し、それを満たすインスタンスを Alloy に発見してもらう。

全ソースはこちら。

exercise-a.3.4.als · GitHub

まずは人間を表すシグネチャ Person を定義する。

sig Person {
  partner: Person,
  shaken: set Person
}

Alloy ではオブジェクトの集合はシグネチャと呼ばれる。シグネチャの宣言は、ある集合と、それにまつわる関係や制約を含む。まずはオブジェクト指向におけるクラスみたいなものだと捉えても問題ない。中括弧の中には Person のフィールドとして partner（パートナー）、shaken（握手をした相手） を宣言している。ある人のパートナーは一人の人間であり、握手をした相手は人間の集合（set）、と定義できる。

このフィールドもまたオブジェクト指向におけるクラスのメンバと考えられるが、面白いのはこれは本質的に Person に属するものではなく、シグネチャ同士の関係として定義される、ということだ。ここでいう関係は、関係データベース（リレーショナルデータベース、RDB）の関係。表とか、タプルの集合をイメージすればよい。フィールドの宣言は関係の宣言であって、partner や shaken は Person に属するわけではないトップレベルの関係として宣言される。

また、partner と shaken はどちらも Person の二項関係であって、shaken における set という多重度キーワードは、ひとつの Person に複数の Person が shaken 関係として対応しうることを表している。RDB で例えるなら、スキーマは同じだがユニーク制約が違うという状況になる。

関係が常に満たす制約は fact キーワードで宣言する。パートナーの関係が対称的であること、自分自身をパートナーにはできないことは、以下のように書ける。

fact partnerProperties {
  partner = ~partner
  no p: Person | p in p.partner
}

ここで特に ~ という記号は、関係の転置を表している。A shaken B ならば常に B shaken A だ。こんなふうに、partner という関係を Person を介さず直接参照することができる。

続いて、アリスとボブを人間の部分集合として宣言する。one キーワードは、宣言した集合の要素がただ一つであることを示す。

one sig Alice, Bob extends Person {}
fact { Alice -> Bob in partner }

アリスとボブがパートナーであることを宣言するために、partner 関係に Alice と Bob の組が含まれていることを（無名の） fact として記述している。

shaken 関係について、shaken 関係が対称的である（握手をするとき、自分もまた握手されている）こと、自分自身とは握手できないこと、パートナーとは握手しないことを制約として与える。

fact shakenProperties {
  shaken = ~shaken
  no p: Person | p in p.shaken
  no p: Person | p.partner in p.shaken
}

ちなみに制約の書き方はひとつではなく、自分自身と握手できないことは

fact { all p: Person | p not in p.shaken }

とか

fact { no shaken & iden }

とか書ける（iden は恒等関係を表す定数）。

この問題の最後の制約として、Alice 以外の参加者が握手した相手の数は互い異なることを宣言する。# は関係の濃度を返す演算子。

fact numShakenPeopleMutuallyDiffer {
  all disj p, p': Person - Alice {
    #p.shaken != #p'.shaken
  }
}

これでモデルの定義は完了。最後に、参加者が 10 人いる状況下でこのモデルの制約を満たすインスタンスが存在するかどうかをチェックする。

pred show {}
run show for exactly 10 Person

run コマンドは与えられた述語を満たすインスタンスを探しだす。ここで指定している述語 show は本体が空なので、これまでに fact として記述された制約だけが適用される。また、run コマンドはスコープの指定を受けとり、探しだすインスタンスのサイズはこのスコープに限られたものとなる。ここでは Person のインスタンスがちょうど 10 であると指定している。

Alloy は制約を満たすインスタンスを発見すると、それをグラフィカルに提示してくれる。そこで得られるのがこちら。

あとは Bob から生えている shaken 関係の辺の数を数えればよい。答えは 4 である。

仕組み

Alloy 自体には問題を解く（充足例や反例を探しだす）機能は実はない。Alloy はユーザの与えた関係と制約からなるモデルから命題論理の式を生成し、外部の SAT ソルバに渡している。Alloy の仕事は、論理式の生成と最適化だ。

インスタンス発見を現実的にするために、Alloy はスコープとしてインスタンスのサイズに制限を与える。先ほどの例ならちょうど 10 の Person だった。このスコープの外に充足例や反例があればもちろんそれは発見できないわけだが、Alloy の作者は「小スコープ仮説」というものを敷いていて、つまり「ほとんどのバグは小さな反例を持つ」という仮説のもとモデリングと検証を行うという思想だ。リーズナブルなトレードオフなんだろうと感じた。

OAuth 2.0 のフローをモデリングする

で、もともとウェブの認証／認可フローを検証したかったわけなので、馴染みのある OAuth 2.0 のフローをモデリングしてみる。……してみたかったわけだけど、どこまで抽象化するというのが難しい。変に抽象度を高めてしまうとその中に暗黙の仮定が入ってしまい、Alloy によって見つけたかったプロトコルの瑕疵が隠れてしまうことも考えられる。結局今回は Authorization Code Grant （よくあるサーバサイドのフロー）において state パラメータがないと、正しくリソースの認可が行えないことを目標にして、簡単のためにかなりの仮定をおいた。

  • OAuth 2.0 の Authorization Code Grant だけを考える
  • URL に含まれるパラメータのやり取りはセキュアに行われるものとして、改竄や漏洩はないものとする
  • redirect_uri はモデリングしない
  • アクセストークンもモデリングしない（リソースオーナと同一視する）
  • 認可サーバとリソースサーバを同一視する
  • ユーザのログイン／ログアウトフローは取り扱わない

などなど。目指す反例もわかっているので、進めやすくはあった。

全ソースは https://github.com/motemen/alloy-sketches/tree/master/oauth2 にあるので、かいつまんで説明する。

今回は時間にともなう状態の変化があるので、時刻を示すシグネチャを宣言する。

open util/ordering[Time]

sig Time {}

util/ordering という特別に最適化された標準モジュールを使って、Time に全順序を導入している。これで next: Time -> Time といった関係が使えるようになる。また、インスタンスを視覚化した際に時刻ごとに別のグラフとして描画し、順を追って見ていくことができる。

認可サーバ（OAuth プロバイダ）はこんな感じにした。登録済みのクライアント（OAuth コンシューマ）およびログイン中のリソースオーナ（ユーザ）は時刻によって変わらないものとした。クライアントに対して発行したコードは時刻によって変化するので Time を含む関係とする。矢印の前後に one や lone とあるのは関係の多重度を表していて、たとえば knownResourceOwners 関係は、ひとつの UserAgent に高々ひとつの ResourceOwner を対応させる。

sig AuthorizationServer {
    knownClients:        ClientId one -> one Client, // 登録済みのクライアント
    knownResourceOwners: UserAgent -> lone ResourceOwner, // ログイン中のリソースオーナ
    issuedCodes:         (Code -> lone Client -> ResourceOwner) -> Time, // 発行したコード
}

状態変化をどうモデリングするかだけど、教科書で紹介されていた方法で、イベントをシグネチャとして表すものを採用した。他の方法も試したけど、今回のように変化する状態が複数ある（プロバイダ側、コンシューマ側）場合はこのやり方がシンプルに書けると思う。

イベントにはつねにユーザエージェントが対応するものとして userAgent、イベント発生前と後の時刻に pre、post フィールドを持たせる。OAuth のフローは HTTP リダイレクトによって次のステップへと進むが、この関係を表すため inParams、outParams、initiator を定義する。

abstract sig Token {}
sig ClientId, ClientSecret, Code, State extends Token {}

abstract sig Event {
    pre, post: Time,
    userAgent: UserAgent, // イベントを引き起こしたユーザエージェント
    inParams:  set Token, // 前のイベントから受けとったパラメータ
    outParams: set Token, // 次のイベントに渡すパラメータ
    initiator: lone Event, // 前のイベント
}

詳しく言うと、イベントは

  • ユーザが OAuth コンシューマを訪問する UserAgentVisitsClientEvent、
  • リダイレクトされたユーザが OAuth プロバイダでコンシューマを認可し、プロバイダが code を発行する AuthorizationServerIssueCodeEvent、
  • さらにリダイレクトされたユーザによってもたらされた code でコンシューマがリソースへのアクセス権を得る ClientAuthorizesUserAgentEvent

と進んで完了、ということにしたいので以下のように定義した（抜粋）。シグネチャのフィールド宣言のあとに中括弧を書くと、そのシグネチャにまつわる fact をシンプルに書ける。

sig UserAgentVisitsClientEvent extends Event { ... } {
    no initiator // fact { all e: UserAgentVisitsClientEvent { no e.initiator } } と同義
    inParams  = none
    outParams = state + client.id
    ...
}

sig AuthorizationServerIssueCodeEvent extends Event { ... } {
    initiator in UserAgentVisitsClientEvent
    inParams  = clientId + state
    outParams = code + state
    ...
}
sig ClientAuthorizesUserAgentEvent extends Event { ... } {
    initiator in AuthorizationServerIssueCodeEvent
    inParams  = code + state
    outParams = none
    ....
}

そしてイベント同士の関連を記述する。イベントの initiator が存在するときは、その outParams を inParams として引き継いでいなければならないとすることで、HTTP リダイレクトの改竄がないことを表現したつもり。また userAgent も同じである、とすれば完全なのだけど、それだと面白みがないので、前のイベントが MaliciousUserAgent によって引き起こされたものであれば、その結果を他のユーザエージェントが引き継いでしまうことを許すことにした。これで悪意あるユーザが他のユーザに CSRF を仕掛けることが可能になる。

fact eventsTakeOverInitiatorsParams {
    all e: Event {
        let e' = e.initiator {
            e.inParams = e'.outParams
            some e' implies { e.userAgent = e'.userAgent or e'.userAgent in MaliciousUserAgent }
        }
    }
}

abstract sig UserAgent {}
sig InnocentUserAgent, MaliciousUserAgent extends UserAgent {}

イベントに基づく状態変化のモデリングは、イディオム的に以下のようにする。

まず2つの時刻間における述語を定義する。その間で状態が変化した場合、対応するイベントが存在しているはず……ということを表現している。

pred step(t, t': Time) {
    some e: Event {
        e.pre  = t
        e.post = t'

        userAgentStates.t        != userAgentStates.t'        iff e in UserAgentVisitsClientEvent
        issuedCodes.t            != issuedCodes.t'            iff e in AuthorizationServerIssueCodeEvent
        obtainedAuthorizations.t != obtainedAuthorizations.t' iff e in ClientAuthorizesUserAgentEvent
    }
}

イベントに対応する fact で状態変化を記述する。

sig UserAgentVisitsClientEvent extends Event { ... } {
    ...
    userAgentStates.post = userAgentStates.pre + client -> state -> userAgent
}

で、これが全ステップ間成り立つことを記す。

pred init(t: Time) {
    no issuedCodes.t
    no obtainedAuthorizations.t
    no userAgentStates.t
}

fact trace {
    init[first]

    all t: Time, t': t.next {
        step[t, t']
    }
}

これでできた。あとは、ユーザエージェントに対してクライアントが取得したリソースが、認可サーバ（リソースサーバ）においてユーザエージェントが保持しているリソースと一致することを assert してチェックする。

assert userAgentsAreProperlyAuthorized {
    all client: Client, userAgent: InnocentUserAgent, resourceOwner: ResourceOwner, t: Time {
        resourceOwner in client.obtainedAuthorizations.t[userAgent] implies {
            let authServer = client.authServer {
                authServer.knownResourceOwners[userAgent] = resourceOwner
                client -> resourceOwner in authServer.issuedCodes.t[Code]
            }
        }
    }
}

check userAgentsAreProperlyAuthorized for 6 but exactly 1 AuthorizationServer, exactly 1 Client, 2 UserAgent

で、実際最後にクライアントがリソースの認可を取得するところで state パラメータのチェックを行わないことにする（コメントアウトする）と、以下のような反例が見つかる。

f:id:motemen:20160630093301p:plain

MaliciousUserAgent のために発行された code でもって他のユーザエージェントが OAuth コンシューマにアクセスすると、そのユーザエージェントのものではないリソースへのアクセス権が得られてしまうような状況が発見できている。つかれた……。

まとめ

Alloy でウェブのフローを部分的にモデリングすることができた。今回は出来上がったものだけがあるのだけど、Alloy はモデルを一気に記述してそのバグを発見するのではなく、ボトムアップに組み立てながら小さいアサーションを繰り返し、インクリメンタルに仕様を作っていくのにこそ向いていると感じた。頑張って書いてみたけど、あとから読めないのではないかというおそれもある。書いたり読んだりするのには熟練が必要だと感じた。

調べてみるとけっこう Alloy を紹介したスライドやらエントリはたくさんあって、知らない世界を覗いた気持ちだった。

参考文献

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

  • 作者:Daniel Jackson
  • 発売日: 2011/07/15
  • メディア: 単行本（ソフトカバー）

形式手法入門―ロジックによるソフトウェア設計―

形式手法入門―ロジックによるソフトウェア設計―

  • 作者:中島 震
  • 発売日: 2012/04/20
  • メディア: 単行本（ソフトカバー）

OAuth2 のフローを Alloy Analyzer でモデリングする - 詩と創作・思索のひろば

参考文献にある形式手法入門は間違いが多いので注意。おすすめできない。

2016/06/30 17:48
b.hatena.ne.jp ……とのこと。

体系的に学ぶ 安全なWebアプリケーションの作り方 脆弱性が生まれる原理と対策の実践

体系的に学ぶ 安全なWebアプリケーションの作り方 脆弱性が生まれる原理と対策の実践

  • 作者:徳丸 浩
  • 発売日: 2011/03/01
  • メディア: 単行本

Go 言語における並行処理の構築部材

Go

5年前に買った『Java並行処理プログラミング ―その「基盤」と「最新API」を究める―』をようやく読んだ。買った頃には Perl やシンプルな JavaScript ばかり書いていたので並行プログラミングなんてほとんど気にすることがなく、実感がなくて読むのも途中で止まってしまっていた本で、家を掃除しているときに見つけたもの。その後も趣味で Android アプリを書くなど Java に触れる機会はあったけれど、せいぜいが AsyncTask を使うくらいで、マルチスレッドを強く意識してコードを書くこともなかった。

Java並行処理プログラミング ―その「基盤」と「最新API」を究める―

Java並行処理プログラミング ―その「基盤」と「最新API」を究める―

ところがここ数年で Go を書きはじめて以来、それと気づかぬ間に並行処理をプログラムするようになっていたのがよかったらしく、今だとあれこれのトピックを身近に感じて興味深く読めた。Go の race detector が優秀で、テキトーなコードの瑕疵を指摘されているうちに感覚が身についてきたのだと思う。

「Share Memory By Communicating」というスローガンでよく表わされるように、Go の並行 API はチャンネルと goroutine によるもので、かなり簡素にできている。一方 Java はsynchronized 修飾子をはじめ、Object#wait / notify とか、インタラプトの仕組みなど、フレームワークとも呼べるような仕組みが用意されていて、対照的だった。しかしそうは言っても goroutine 間で変数を共有したいことは Go を書いていても頻繁にあるわけで、参考になるところは多い。

この本では正しい並行処理を行うために、

  • データの不変項をカプセル化し、それを構成する変数を同じロックでガードすること
  • API の同期化ポリシーをドキュメントすること

を推奨している。特に後者。利用者は API の形式的な情報からそのスレッドセーフ性を判断することができないからだ。Go の標準ライブラリでも、並行処理に関わりそうなところではその旨ドキュメントされているみたいだ。

% go doc strings.Replacer
type Replacer struct {
        // Has unexported fields.
}
    Replacer replaces a list of strings with replacements. It is safe for
    concurrent use by multiple goroutines.
% go doc net/http2.Framer.WriteData
func (f *Framer) WriteData(streamID uint32, endStream bool, data []byte) error
    WriteData writes a DATA frame.

    It will perform exactly one Write to the underlying Writer. It is the
    caller's responsibility to not call other Write methods concurrently.

以下、一般的な並行処理の構築部材（ビルディングブロック）を Go でどう実現するかのパターンをメモしておく。Go 的にはこういった処理はライブラリ化するのではなくコピペもしくはイディオムとして憶えておくのが正しい態度だろうので、過度の一般化をしようとしてはいけない。

見聞きして知っていることをもとにできるだけ真摯に書くが、現実世界の並行プログラミングに詳しいわけではないので間違っていることもあるかもしれない。

ミューテックス（Mutex）

ミューテックスは複数のスレッド間で共有するリソースのアクセス権を管理する部品。これはそのまま sync.Mutex というのが存在する。チャンネルに依らない同期を行うのにたいへん重要なでプリミティブな部品だ。

sync.Mutex は zero value が未ロックを表していて、特別な初期化を必要としないので構造体に埋め込むことができる。

type syncMap struct {
    sync.Mutex
    m map[string]string
}

など。この構造体 s のフィールドを変更する前と後に s.Lock() と s.Unlock() を呼ぶよう徹底できていれば、この構造体は goroutine セーフだと言える。もちろんこれらのフィールドはプライベートにしておくべきである。

構造体を作るほどではない時は、守りたい変数と並べて宣言しておく。同じ括弧の中に入れるとよりよいと思う。Mutex の Go における短い名前は「mu」である。

var (
    cache map[string]string
    cacheMu sync.Mutex
)

Read-Write ロックを実現するための RWMutex というのもある。

ラッチ（Latch）

ラッチは条件が整うまでスレッドの実行を留めておくための部品。たとえば全ての HTTP GET が終わってデータが揃うまでは待機する、というようなときに使う。

これは Go においては sync.WaitGroup という名前で提供されている。これも zero value で意味を持つので、var wg sync.WaitGroup と宣言して使う。

典型的には以下のように使われる。

var wg sync.WaitGroup
for _, arg := range args {
    wg.Add(1)
    go func(arg string) {
        longRunningTask(arg)
        wg.Done()
    }(arg)
}
wg.Wait()
...

WaitGroup の Go における短い名前は「wg」である。ちなみに複数の goroutine を起動してすべての処理が完了するまで待つとき、その数があらかじめわかっている場合は、結果を通知するチャンネルを利用することもある。

c := make(chan struct{}, 4)
for i := 0; i < 4; ++i {
    go doJob(i, c) // 終わったら c <- struct{}{} される
}
for i := 0; i < 4; ++i {
    <-c
}

ブロッキングキュー（Blocking Queue）

有限または無限のキャパシティを持つキューで、キャパシティを越えて追加しようとするとき及び空の状態で取り出そうとするときにブロックする。2つのプロセスでリソースの所有権を移動しながら同期化できる。

Go おいてはこれこそがチャンネル（chan）。自明なのでコードは特になし。チャンネルの Go における短い名前は「c」である（「ch」もないわけではない）。

セマフォ（Semaphore）

（計数）セマフォは決まった数のプロセスだけが同時に並行に走ってよい、という制限を設けるためのもの。たとえば過剰な IO を避けるために利用される。

Go においてセマフォはキャパシティありのチャンネルとして実装できる。

var sem = make(chan struct{}, maxConcurrency)

func process(arg string) {
    sem <- struct{}{}
    ...
    <-sem
}

func run() {
    for _, arg := range args {
        go process(arg)
    }
}

これ初めて見たときはよく分かんなかった。セマフォの Go における短い名前は「sem」である。

Future

Future （カタカナで書かない気がする）は後々必要になる値の計算や IO をあらかじめスタートさせておきたいような場合に使うパターン。結果を取得するときにブロックさせて待つこともできる。自分は実際に書いたり読んだりした経験はないのだけど、Future パターンを意識して書くならこんな風に書けると思う。

struct futureInt {
    result int
    done chan struct{}
}

func (fut *futureInt) Get() int {
    <-fut.done
    return fut.result
}

func calcInt() futureInt {
    fut := futureInt{
        done: make(chan struct{}),
    }
    go func() {
        fut.result = longRunningTask()
        close(fut.done)
    }
    return fut
}

バリヤ（Barrier）

こちらは参考までに記しておく。Java の CyclicBarrier というクラスは再利用のできるラッチのようなもので、スレッド群を繰り返し同期化するような場合に便利らしい。

検索すると sync.Cond を使ったあまり簡単ではない例も見つかるのだが、golang-dev には goroutine は十分軽量だから毎回新しいのを起動したらいいよ といった話もあり、そっちのほうが Go らしいようにも思った。

まとめ

プログラム言語の話に限らず、ある領域の見聞や経験を深めたあとでは他の領域から得られる知識の吸収の仕方の質が異なるもので、思ったより参考になる話が多かった。とはいえ Go には Go のやり方があるものなので、あまり Java におけるクラスやパターンをそのまま流用しようとするのはよくない傾向であることも意識しておかなければならない。Go を読み書きする際には（パターンというほどでもない）イディオムを知っておくことに意味がある言語なので、こうやってまとめておくことも無駄ではないだろうと思う。

参考文献

Java並行処理プログラミング ―その「基盤」と「最新API」を究める―

Java並行処理プログラミング ―その「基盤」と「最新API」を究める―

増補改訂版 Java言語で学ぶデザインパターン入門 マルチスレッド編

増補改訂版 Java言語で学ぶデザインパターン入門 マルチスレッド編

AsciiDoc（Asciidoctor）の文書をtextlintで校正する

JavaScript Ruby

AsciiDocはMarkdownのようなテキストマークアップ言語のひとつで、ページ内リンクや脚注などかなり機能が豊富なので、大きめのドキュメントを本腰を入れて書くなど、表現したいものがある程度複雑なときに便利。DocBookというフォーマットを通じて、HTMLだけでなくPDFとかroff形式にも変換できるらしい（やったことはない）。GitのドキュメントがAsciiDoc形式で書かれているのを見て知って、自分も個人的なドキュメントはREADME.adocなどとして、AsciiDoc形式で書くことがある。AsciidoctorはAsciiDocの実装のひとつで、Rubyで書かれていて利用が簡単なのでこれを使っている。

さて、上記の記事でtextlintなるものを知ったので、AsciidoctorのJavaScript実装を使ってプラグインを書こうと思いたったわけだ（標準で対応しているのはプレーンテキスト、HTML、Markdownのみ）。しかし取りかかってみるとこれがなかなか大変で、textlintの期待するデータ構造はテキストの行やカラム位置の情報まで求めるので、Asciidoctorのパーザに精通している必要がありそうだった。せいぜい校正項目のある行くらいが分かれば自分の目的は達成されるので、ここまでやるのは少し苦労が多そうだった。

そこで、一度プレーンテキストに変換してからtextlintで処理し、結果のエラーの行番号を元のファイルの行にマッピングする、という方法を取ることにしたのがこちら。npm install textlint してある前提。

Rubyのスクリプトで、指定されたファイルをAsciidoctorのAPIで解析し、構文木をたどりながらプレーンテキストを吐く。その際に各行と、そのソースの位置情報を記録しておく。プレーンテキストに対してtextlintを走らせて、結果をJSONで受けとり、元のファイル名に直して出力する。そのままVimのquickfixリストにできるフォーマット。

少しだけ変なハックを入れている。このスクリプトは通常はHTMLタグのみを消して出力する、つまりアンカーテキストなどは校正の対象となるのだけど、それで上手くいかない場合があった。codeタグの中に入ったアルファベットも日本語のルールで校正されてしまう、という問題だ。そこで -T オプションでそのタグの内容を墨塗りできるようにしてある。中身を消し去ってしまうと変な文章になるので、苦肉の策。墨塗り文字のくり返しがエラーになるので、そいつは無視する、ということもしている。

はてなで一緒に働きませんか？