Page 135 - My FlipBook
P. 135
、字串限制式求解 Brochure 2020
133
網路程式安全是我們數位基礎建設的關鍵基石。在
所有確保網路安全的方法中，自動化的網路程式安
全分析明顯的有很高的需求。字串限制式求解器可
以說是新一代自動化網路安全分析技術的引擎。在
這樣的高度需求下，近六年來，有大量關於這個主
題的研究發表。我們和一些在歐洲的合作者，在這
個題目上取得了一系列的成果。舉例來說，我們將
Craig 在 1957 年在數理邏輯提出的內插理論擴展到
字串限制式，這是軟體模型驗證的關鍵技術，可以
用來自動產生迴圈不變量。我們所開發的字串限制
式求解器 Trau 目前是全世界最有效率的實作之一。
儘管如此，網路程式分析對於字串限制式求解器效
能有很高的要求，目前求解器的發展仍然和實際的
完整需求有明顯的落差。我們正和全世界此領域的
研究者密切共同合作，以期待能縮小這個差距。
五、敏感資料之群組共享
隱私保護的意涵不僅在於個人資料取得上的限制，
同時也在於資訊使用與揭露的原則與規範。妥善管
理資訊流向、鼓勵資料分享、並維持所分享資訊的
私密性，可真是挑戰。一般作法是透過集中式的資
料控制單位，將來自眾多個人的資料集去識別化後，
再行釋出供二次使用。不過，這三方⸺
133
網路程式安全是我們數位基礎建設的關鍵基石。在
所有確保網路安全的方法中，自動化的網路程式安
全分析明顯的有很高的需求。字串限制式求解器可
以說是新一代自動化網路安全分析技術的引擎。在
這樣的高度需求下，近六年來，有大量關於這個主
題的研究發表。我們和一些在歐洲的合作者，在這
個題目上取得了一系列的成果。舉例來說，我們將
Craig 在 1957 年在數理邏輯提出的內插理論擴展到
字串限制式，這是軟體模型驗證的關鍵技術，可以
用來自動產生迴圈不變量。我們所開發的字串限制
式求解器 Trau 目前是全世界最有效率的實作之一。
儘管如此，網路程式分析對於字串限制式求解器效
能有很高的要求，目前求解器的發展仍然和實際的
完整需求有明顯的落差。我們正和全世界此領域的
研究者密切共同合作，以期待能縮小這個差距。
五、敏感資料之群組共享
隱私保護的意涵不僅在於個人資料取得上的限制，
同時也在於資訊使用與揭露的原則與規範。妥善管
理資訊流向、鼓勵資料分享、並維持所分享資訊的
私密性，可真是挑戰。一般作法是透過集中式的資
料控制單位，將來自眾多個人的資料集去識別化後，
再行釋出供二次使用。不過，這三方⸺
