The 3rd Joint Seminar on Programming Languages and Systems


第三屆程式語言暨系統研討會

Sponsored by
NTU/NSC Center of Excellence for Research in Computer Systems, and
Institute of Information Science, Academia Sinica


台灣大學 電腦系統技術研發重點中心
中央研究院 資訊科學研究所
合辦

March 5, 1999


Schedule

10:00 -- 11:00
Towards An Engineering of Proofs
Jean-Pierre Jouannaud, Universit'e de Paris-Sud`a Orsay
11:00 -- 12:00
SGM: A User-Friendly Verification Environment
熊博安 中央研究院 資訊科學研究所 (Poa-Ann Hsiung, Academia Sinica)
13:30 -- 14:30
InterRISC: An Integrated Environment for Learning Programming Languages
陳日昌 義守大學 資訊工程學系 (Jichang Tan, I-Shou University)
14:30 -- 15:30
Type System Attack against Software Security
黃世昆 中央研究院 資訊科學研究所 (Shih-Kun Huang, Academia Sinica)
 

Purposes


This seminar series aims to bring together researchers and students working on programming languages and systems to present results in their fields. It hopes to provide a stimulating environment to further facilitate the exchange of ideas and experiences among the participants.


Further Information

The seminar will be held at 台北市 南港區 中央研究院 資訊科學研究所 107 會議室 on March 5 (Friday), 1999.
Direction to the seminar location is available at http://www.sinica.edu.tw/as/map/index_c.html

Students are especially welcomed to attend this seminar series. There is no registration fee and lunches will be provided. To help plan the event, however, please send a plain text e-mail to trc@iis.sinica.edu.tw with your name and current affiliation if you plan to attend.

Further information about this event, including abstracts of the talks, is available from WWW at http://www.iis.sinica.edu.tw/~trc/plas1999.html


Abstracts

SGM: A User-Friendly Verification Environment

熊博安 中央研究院 資訊科學研究所 (Poa-Ann Hsiung, Academia Sinica)

Model-checking often faces the problem of reducing large exponential sizes of state-space representations. Several reduction techniques such as bisimulation equivalence, partial-order semantics, and symmetry-based reduction have been proposed, but existing verification tools do not completely allow a user flexibility in manipulating state-spaces. We propose a new user-friendly verification environment where a user has full control on what techniques to apply and in what sequences to apply them. We have implemented the environment in a tool called "State-Graph Manipulators" (SGM). SGM packages verification techniques into efficient, reusable, modular "manipulators", that act on high-level state-space representations called "state-graphs". Without being a verification expert, a user can still use the graphical interface of SGM to manipulate state-graphs for better verification efficiency. Thus, SGM tries to bridge the gap between profound verification theory and practical use of verification. Further, we are also proposing three new state-space reduction techniques, namely Read-Write Analysis, Bypass Internal Transitions, and Sibling Transition Multiplicity Reduction. They are implemented into SGM and experiments have been conducted to show their usefulness.

Some related tool information:

SGM is currently in its v1.2 release and is available for free download at http://www.iis.sinica.edu.tw/~eric/sgm/. SGM v1.2 has been licensed for free education/research use by over 110 people from around 20 countries in the world. SGM is also listed in the Virtual Library of Formal Methods and Tools along with internationally famous tools like SMV, Uppaal, Kronos, Hytech, etc.


InterRISC: an Integrated Environment for Learning Programming Languages

陳日昌 義守大學 資訊工程學系 (Jichang Tan, I-Shou University)

Hand-on experience is essential in learning programming languages. The process can be more useful if testing is also available to
evaluate the levels of understanding. However, this is not supported in ordinary programming environments. In this talk, we show how such need can be integrated in a system called InterRISC. For learning low-level programming languages like assembly and C, InterRISC is designed to be more user-friendly and learning-centric. For example, syntax errors are prevented by the graphic user interface and the process is guided by examples and high-level specifications. Based on our two-year experience, this approach can effectively help self-learning and reduce substantial manpower in result evaluation. Besides the demonstration, we shall also discuss the possible pitfalls and applications in using a system like this one. (If interested, please find the latest versions of InterRISC at http://taurus.csie.isu.edu.tw/asm.)


Type System Attack against Software Security

黃世昆 中央研究院 資訊科學研究所 (Shih-Kun Huang, Academia Sinica)

Current trends of network attacks are focusing on exploitation of computer system vulnerabilities, including TCP/IP specification and implemtation defects, exceptions on software fault, and inconsideration of system administration.

The fault of buffer overflow is the primary source of software system vulnerability. In many situations, when a system is vulnerable to the overflow attack, exploits and security threat will be made possible by injecting malicious code into the system. Type inconsistency between inter-module invocations will give rise to instability of software systems. It can also be exploited to generate potential security flaws.

In my talk, I will introduce techniques to explore type system problems during program linkage and how to apply theorem prover for inspecting language design flaws. They can be used to analyze Web system security and static checking for run-time errors.