From owner-soc-status@FreeBSD.ORG Sun May 29 20:43:40 2011 Return-Path: Delivered-To: soc-status@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:4f8:fff6::34]) by hub.freebsd.org (Postfix) with ESMTP id 92BC11065672 for ; Sun, 29 May 2011 20:43:40 +0000 (UTC) (envelope-from m.kocielski@gmail.com) Received: from mail-ey0-f182.google.com (mail-ey0-f182.google.com [209.85.215.182]) by mx1.freebsd.org (Postfix) with ESMTP id E3AA58FC0C for ; Sun, 29 May 2011 20:43:39 +0000 (UTC) Received: by eyg7 with SMTP id 7so1555809eyg.13 for ; Sun, 29 May 2011 13:43:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:date:x-google-sender-auth :message-id:subject:from:to:cc:content-type; bh=4zM3xJidj2QAVxGpVEdsXheS+oEpUr6liKTM/xkqzRU=; b=de8FPqB5UfCv2T3ktsORBJlWvgg1JaTGyuv5qZ7jG6X1nfTeaGexQUdivuVTjnkFJQ RrMnc9i9vKHQUavbIlzS4gF6T8Itn8hbJxRwOKHS86kX78djymGdZWlzUHsIppdu7OPZ ZsuBmuN9Lbk8bhk4AkAghTligQvGWeNeOizTU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:cc:content-type; b=vUKZ07h/BlxudLfcbOq4Nk69UDYIqGLTLhNF6XUwdEmqq4pOnpE0tgH+wngzIz+d/J xqrg4FSXEAs1hHzSFjLCFkX9vTCxrI/EpWKIcxOco0W3OvXNg7uEii/In+B7q3uyISKy lXkV8i8Q3WkpKtToeqyI0MoTs4+2YOyf7Xp4w= MIME-Version: 1.0 Received: by 10.213.112.196 with SMTP id x4mr662340ebp.108.1306700261950; Sun, 29 May 2011 13:17:41 -0700 (PDT) Sender: m.kocielski@gmail.com Received: by 10.213.32.81 with HTTP; Sun, 29 May 2011 13:17:41 -0700 (PDT) Date: Sun, 29 May 2011 22:17:41 +0200 X-Google-Sender-Auth: rVnxGJNkxoUz-oSDmP0QyrraCsQ Message-ID: From: Mateusz Kocielski To: soc-status@freebsd.org Content-Type: text/plain; charset=ISO-8859-1 Cc: "Robert N. M. Watson" Subject: Testing temporal properties with Temporally Enhanced Security Logic Assertions - week 1 X-BeenThere: soc-status@freebsd.org X-Mailman-Version: 2.1.5 Precedence: list List-Id: Summer of Code Status Reports and Discussion List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 29 May 2011 20:43:40 -0000 Hello, My project is Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA). Its wikipage is available at [1]. You can find there more information on project as well as schedule and links to repository. What was done this week: - writing test cases for the TeslaInsrumenter - setting up testing environment (on kvm) - writing basic examples of using TESLA (userland) My plans for the next week: - move testing environment to virtualbox - polish up test suite for the TeslaInstrumenter (discuss it with TI developers) - write some basic tesla assertions for the kernel and test it - read MAC framework code - write schedule for MAC framework testing - (hopefully) start MAC testing (e.g. replace mac_test module with tesla automata) Please contact me in case of any questions. Usually best way of communication with me is IRC, I'm shm at freenode. [1] - http://wiki.freebsd.org/ShmSoc2011 Regards, Mateusz Kocielski