Snowdream

http://blog.yxwang.me/

寫了好幾天的代碼因?yàn)檫€有bug沒(méi)de掉，沒(méi)commit到svn上

然后不知怎么的在make的時(shí)候生成的kernel沒(méi)變化，于是直接make world，然后發(fā)現(xiàn)linux kernel目錄被清空了。。。

只能明天靠記憶慢慢補(bǔ)了，皚皚。

yifanw大牛半個(gè)月前發(fā)在c++版上的，怕以后忘了看先放在這備個(gè)忘吧

白話入門
http://www.newsmth.net/bbscon.php?bid=335&id=250203

白話解決方案
http://www.newsmth.net/bbscon.php?bid=335&id=250237

白話參考文獻(xiàn)
http://www.newsmth.net/bbscon.php?bid=335&id=250260

最近有點(diǎn)忙，今天總算在某個(gè)課題deadline前把論文憋出來(lái)交上去了。跑這兒來(lái)推薦兩篇上個(gè)月看到的比較有意思的paper，都比較偏理論，也很老。

今天寫介紹下第一篇，劍橋大學(xué)的A Logic of Authentication，中了SOSP '89，整理后發(fā)在1990年的ACM Transactions on Computer Systems上。
http://www.csie.fju.edu.tw/~yeh/research/papers/os-reading-list/burrows-tocs90-logic.pdf

（另一篇是Safe Kernel Extensions Without Run-Time Checking，改天再寫點(diǎn)介紹）

這篇paper的主要工作是通過(guò)構(gòu)造一種多種類的模態(tài)邏輯(many-sorted model logic)，來(lái)檢查網(wǎng)絡(luò)中驗(yàn)證協(xié)議的安全性。

基礎(chǔ)的邏輯分三部分：
原語(yǔ)，如驗(yàn)證雙方A和B，以及服務(wù)器S，下文用P Q R泛指
密鑰，如K_ab代表a和b之間的通訊密鑰，K_a代表a的公鑰，{K_a}^{-1}代表對(duì)應(yīng)的私鑰，下文用K泛指
公式（或者陳述），用N_a, N_b等表示，下文用X Y泛指

接下來(lái)定義以下約定（constructs）
P 信任 X: 原語(yǔ)P完全信任X
P 看到 X: 有人發(fā)送了一條包含X的信息給P，P可以閱讀它或者重復(fù)它（當(dāng)然通常是在做了解密操作后）
P 說(shuō)了 X: 原語(yǔ)P發(fā)送過(guò)一條包含X的信息，同時(shí)也可以確定P是相信X的正確性的
P 控制 X: P可以判定X的正確與否。例如生成密鑰的服務(wù)器通常被默認(rèn)為擁有對(duì)密鑰質(zhì)量的審核權(quán)。
X 是新鮮的: 在此之前X沒(méi)有被發(fā)送過(guò)。這個(gè)事實(shí)可以通過(guò)綁定一個(gè)時(shí)間戳或者其他只會(huì)使用一次的標(biāo)記來(lái)證明。
P <-K-> Q: P和Q可以通過(guò)共享密鑰K進(jìn)行通訊，且這個(gè)K是好的，即不會(huì)被P Q不信任的原語(yǔ)知道。
K-> P: P擁有K這么一個(gè)公鑰，且它對(duì)應(yīng)的解密密鑰K^{-1}不會(huì)被其他不被P信任的原語(yǔ)知道。
P <=X=> Q: X是一個(gè)只被P和Q或者P和Q共同信任的原語(yǔ)知道的陳述，只有P和Q可以通過(guò)X來(lái)相互證明它們各自的身份，X的一個(gè)例子就是密碼。
{X}_K: X是一個(gè)被K加密了的陳述
<X>_Y: 陳述X被Y所綁定，Y可以用來(lái)證明發(fā)送X的人的身份

好了，總算把這些約定列完了，然后來(lái)看看通過(guò)這些約定能推出一些什么東東：
如果 P 相信 (P <-K-> Q), 且 P 看到 {X}_K，那么 P 相信 Q 說(shuō)了 X。
這個(gè)例子很簡(jiǎn)單，既然P Q有安全的密鑰K，那么P看到通過(guò)K加密后的X肯定認(rèn)為就是Q發(fā)出的。

又比如，
如果 P 相信 Q 控制 X，P 相信 (Q 相信 X)，那么 P 相信 X
也很容易理解，既然 P 相信 Q 的判斷，那么 Q 相信什么 P 自然也就相信了。

再舉一個(gè)例子
如果 P 相信 Y 是新鮮的，那么 P 相信 (X, Y) 也是新鮮的。
這里(X, Y)表示 X 和 Y 的簡(jiǎn)單拼接，也很容易理解，既然 Y 之前沒(méi)出現(xiàn)過(guò)，那么 X 和 Y 的組合自然也沒(méi)出現(xiàn)過(guò)。

一個(gè)協(xié)議要被定義為安全，最起碼要滿足
A 相信 A <-K->B，B 相信 A <-K->B
即雙方要互相信任密鑰是安全的

再健壯一點(diǎn)的協(xié)議，還要滿足
A 相信 (B 相信 (A 相信 A <-K->B))，反之一樣
即A B不僅相信密鑰，也相信對(duì)方相信自己對(duì)密鑰的信任。

有了這些簡(jiǎn)單卻強(qiáng)大的工具后，接下來(lái)這篇paper開始著手分析一些協(xié)議，包括Kerberos協(xié)議，Andrew Secure RPC 握手協(xié)議等，還指出了其中的一些問(wèn)題和改進(jìn)措施，例如CCITT X.509 協(xié)議中可以通過(guò)重復(fù)發(fā)送一條老的信息來(lái)模仿成加密雙方中的一員。

具體的分析不貼上來(lái)了，一方面對(duì)于我這個(gè)不熟悉TeX的人來(lái)說(shuō)碼公式實(shí)在麻煩，另一方面我實(shí)在困死了 =_=

建議有興趣的朋友好好看看這篇經(jīng)典paper

Some notes on lock-free and wait-free algorithms

http://www.audiomulch.com/~rossb/code/lockfree/

?

NOBLE - a library of non-blocking synchronization protocols

http://www.cs.chalmers.se/~noble/

?

An optimistic approach to lock-free FIFO queues (Distributed Computing 2008)

http://people.csail.mit.edu/edya/publications/OptimisticFIFOQueue-journal.pdf

?

High performance dynamic lock-free hash tables and list-based sets

http://portal.acm.org/citation.cfm?id=564870.564881

?

Concurrent Programming Without Locks

http://www.cl.cam.ac.uk/research/srg/netos/papers/2007-cpwl.pdf

?

Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms

http://www.research.ibm.com/people/m/michael/podc-1996.pdf

抓抓大牛的博客(http://www.cnblogs.com/JeffreyZhao)上看到的鏈接，原文地址是
http://blog.objectmentor.com/articles/2009/02/26/10-papers-every-programmer-should-read-at-least-twice

貌似我只讀過(guò)那篇Reflections on Trusting Trust，水木的Programming版搜索作者為modico的帖子的前四篇就是介紹這篇paper的。

先貼個(gè)列表，改天好好讀一讀

1. On the criteria to be used in decomposing systems into modules – David Parnas
2. A Note On Distributed Computing – Jim Waldo, Geoff Wyant, Ann Wollrath, Sam Kendall
3. The Next 700 Programming Languages – P. J. Landin
4. Can Programming Be Liberated from the von Neumann Style? – John Backus
5. Reflections on Trusting Trust – Ken Thompson
6. Lisp: Good News, Bad News, How to Win Big – Richard Gabriel
7. An experimental evaluation of the assumption of independence in multiversion programming – John Knight and Nancy Leveson
8. Arguments and Results – James Noble
9. A Laboratory For Teaching Object-Oriented Thinking – Kent Beck, Ward Cunningham
10. Programming as an Experience: the inspiration for Self – David Ungar, Randall B. Smith

作者博客后面還新增了對(duì)它們的簡(jiǎn)要評(píng)論

2009-01-08

今年的ASPLOS '09上zhou yuanyuan也有一篇關(guān)于如何concurrent program中發(fā)現(xiàn)隱藏的atomicity violation bugs的paper，里面提到了這篇paper

2008-11-30

OSDI '08上MSR發(fā)的paper，針對(duì)并發(fā)編程中難以發(fā)現(xiàn)的bug問(wèn)題。

paper的內(nèi)容主要分兩大塊。

一是如何在發(fā)現(xiàn)bug的時(shí)候記錄下線程的運(yùn)行先后(thread interleaving)，途徑是在線程API和用戶程序多寫一層wrapper functions，這里還有一些其他的問(wèn)題，比如只記錄下了thread interleaving的話出現(xiàn)data race怎么解決等。

另外一塊內(nèi)容是如何遍歷出給定程序運(yùn)行后所能產(chǎn)生的結(jié)果的集合，加入這個(gè)能實(shí)現(xiàn)的話那就能把所有隱藏的bug都找出來(lái)了。但是這個(gè)搜索空間很大，是 指數(shù)級(jí)的，的一個(gè)結(jié)論就是：給定一個(gè)程序有n個(gè)的線程，所有線程共完成k條指令，那么c次占先調(diào)度后線程的排列情況數(shù)的復(fù)雜度是的，所以在實(shí)現(xiàn)遍歷代碼的時(shí)候必須有效的降低k和c的值。

問(wèn)題現(xiàn)象：上校內(nèi)、一些國(guó)內(nèi)論壇時(shí)經(jīng)常出現(xiàn)連接重置(Connect reset)錯(cuò)誤，而上google baidu等網(wǎng)站卻沒(méi)什么問(wèn)題。ping那些有問(wèn)題的網(wǎng)站的結(jié)果很正常。

google了一堆關(guān)鍵詞后終于發(fā)現(xiàn)問(wèn)題出在MTU上，至少在偶的本本上運(yùn)行
sudo ifconfig eth1 mtu 1412
就沒(méi)問(wèn)題了（eth1是無(wú)線網(wǎng)卡）

p.s 多謝萬(wàn)熊? XD

     摘要: 發(fā)信人: linelf (水水), 信區(qū): Real_Estate
標(biāo) 題: 蘇南經(jīng)濟(jì)模式興衰親歷記zz
發(fā)信站: 日月光華 (2009年01月15日20:39:22 星期四)

  閱讀全文