Path: csiph.com!v102.xanadu-bbs.net!xanadu-bbs.net!news.glorb.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!news.iecc.com!.POSTED!nerds-end From: Seima Rao Newsgroups: comp.compilers Subject: Formulating Security in Programming Languages Date: Thu, 15 Jan 2015 17:49:53 +0530 Organization: Compilers Central Lines: 32 Sender: news@iecc.com Approved: comp.compilers@iecc.com Message-ID: <15-01-014@comp.compilers> NNTP-Posting-Host: news.iecc.com Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Trace: miucha.iecc.com 1421421558 70231 2001:470:1f07:1126:0:676f:7373:6970 (16 Jan 2015 15:19:18 GMT) X-Complaints-To: abuse@iecc.com NNTP-Posting-Date: Fri, 16 Jan 2015 15:19:18 +0000 (UTC) Keywords: question Posted-Date: 16 Jan 2015 10:19:18 EST X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com Xref: csiph.com comp.compilers:1471 Hi, I came up with this notation in stating the goal of security in programming languages: Programming Language Construct = Syntax + Semantics + Side Effect. N# semantics N# syntax = Syntax + Semantics + Side Effects Security = N# semantics N# syntax - Side Effects I will explain via a C example: N# (malloc-semantics) N# (malloc-syntax, free-opt-syntax) = Memory Allocation + Memory Deallocation + Memory Leak In the above, the LHS says, apply the combined syntaxes of malloc and optional-free to the semantics of malloc. The result is that Memory Leak is a side effect. So, the goal of security is to remove Memory Leaks. Does the approach specified in the above paragraphs occur to you as brute force esp when generalizing over the entire grammar(small & manageable) if not the semantics(the whole large LRM)? Is anyone interested in this topic ? Are there any other formal approaches to investigating security in Programming Languages? Sincerely, Seima Rao.